At: quotient of nsubn 2 1 2 1 1 1
1. n: {1+1...}
2. 
E:(
(n-1)
(n-1)Prop).
(EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) 
(
m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))
3. E: nnProp
4. EquivRel x,y:n. x E y
5. x,y:n. Dec(x E y)
6. EquivRel x,y:(n-1). x E y
7. m: (n-1+1)
8. f: m(i,j:(n-1)//(i E j))
9. g: (i,j:(n-1)//(i E j))m
10. InvFuns(m; i,j:(n-1)//(i E j); f; g)
11. x: m
f(x) 
i,j:n//(i E j)
By: BackThru
Thm* n:{1...}, m:n, E:(nnProp).
(EquivRel x,y:n. x E y) (z:x,y:m//(x E y). z x,y:n//(x E y))
Generated subgoals:None
About:
