let n be Element of NAT ; :: thesis: len (Decomp (n,2)) = n + 1
deffunc H₁( Nat) -> set = <*$1,(n -' $1)*>;
consider q being FinSequence such that
A1: len q = n and
A2: for k being Nat st k in dom q holds
q . k = H₁(k) from FINSEQ_1:sch 2();
A3: dom q = Seg n by A1, FINSEQ_1:def 3;
set q1 = q ^ <*<*0,n*>*>;
A4: dom q = Seg n by A1, FINSEQ_1:def 3;
A5: len (q ^ <*<*0,n*>*>) = n + 1 by A1, FINSEQ_2:16;
then A6: dom (q ^ <*<*0,n*>*>) = Seg (n + 1) by FINSEQ_1:def 3;

now :: thesis: for x1, x2 being object st x1 in dom (q ^ <*<*0,n*>*>) & x2 in dom (q ^ <*<*0,n*>*>) & (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (q ^ <*<*0,n*>*>) & x2 in dom (q ^ <*<*0,n*>*>) & (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 implies x1 = x2 )
assume that
A7: x1 in dom (q ^ <*<*0,n*>*>) and
A8: x2 in dom (q ^ <*<*0,n*>*>) and
A9: (q ^ <*<*0,n*>*>) . x1 = (q ^ <*<*0,n*>*>) . x2 ; :: thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A7, A8;
x2 in (Seg n) \/ {(n + 1)} by A6, A8, FINSEQ_1:9;
then A10: ( x2 in Seg n or x2 in {(n + 1)} ) by XBOOLE_0:def 3;
x1 in (Seg n) \/ {(n + 1)} by A6, A7, FINSEQ_1:9;
then A11: ( x1 in Seg n or x1 in {(n + 1)} ) by XBOOLE_0:def 3;

now :: thesis: x1 = x2

per cases ( ( x1 in Seg n & x2 in Seg n ) or ( x1 in Seg n & x2 = n + 1 ) or ( x1 = n + 1 & x2 in Seg n ) or ( x1 = n + 1 & x2 = n + 1 ) ) by A11, A10, TARSKI:def 1;

suppose A12: ( x1 in Seg n & x2 in Seg n ) ; :: thesis: x1 = x2

then A13: ( (q ^ <*<*0,n*>*>) . k1 = q . k1 & (q ^ <*<*0,n*>*>) . k2 = q . k2 ) by A3, FINSEQ_1:def 7;
( q . k1 = <*k1,(n -' k1)*> & q . k2 = <*k2,(n -' k2)*> ) by A2, A4, A12;
hence x1 = x2 by A9, A13, FINSEQ_1:77; :: thesis: verum

end;

suppose A14: ( x1 in Seg n & x2 = n + 1 ) ; :: thesis: x1 = x2

then A15: (q ^ <*<*0,n*>*>) . k2 = <*0,n*> by A1, FINSEQ_1:42;
(q ^ <*<*0,n*>*>) . k1 = q . k1 by A3, A14, FINSEQ_1:def 7
.= <*k1,(n -' k1)*> by A2, A4, A14 ;
then k1 = 0 by A9, A15, FINSEQ_1:77;
hence x1 = x2 by A14, FINSEQ_1:1; :: thesis: verum

end;

suppose A16: ( x1 = n + 1 & x2 in Seg n ) ; :: thesis: x1 = x2

then A17: (q ^ <*<*0,n*>*>) . k1 = <*0,n*> by A1, FINSEQ_1:42;
(q ^ <*<*0,n*>*>) . k2 = q . k2 by A3, A16, FINSEQ_1:def 7
.= <*k2,(n -' k2)*> by A2, A4, A16 ;
then k2 = 0 by A9, A17, FINSEQ_1:77;
hence x1 = x2 by A16, FINSEQ_1:1; :: thesis: verum

end;

suppose ( x1 = n + 1 & x2 = n + 1 ) ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

then q ^ <*<*0,n*>*> is one-to-one by FUNCT_1:def 4;
then A18: card (rng (q ^ <*<*0,n*>*>)) = n + 1 by A5, FINSEQ_4:62;
A19: rng q c= rng (q ^ <*<*0,n*>*>) by FINSEQ_1:29;
A20: rng (q ^ <*<*0,n*>*>) = { <*i,(n -' i)*> where i is Element of NAT : i <= n }

proof

thus rng (q ^ <*<*0,n*>*>) c= { <*i,(n -' i)*> where i is Element of NAT : i <= n } :: according to XBOOLE_0:def 10 :: thesis: { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= rng (q ^ <*<*0,n*>*>)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (q ^ <*<*0,n*>*>) or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } )
assume x in rng (q ^ <*<*0,n*>*>) ; :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then consider j being Nat such that
A21: j in dom (q ^ <*<*0,n*>*>) and
A22: (q ^ <*<*0,n*>*>) . j = x by FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
j in (Seg n) \/ {(n + 1)} by A6, A21, FINSEQ_1:9;
then A23: ( j in Seg n or j in {(n + 1)} ) by XBOOLE_0:def 3;

now :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }

per cases ( j in Seg n or j = n + 1 ) by A23, TARSKI:def 1;

suppose A24: j in Seg n ; :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }

then A25: (q ^ <*<*0,n*>*>) . j = q . j by A3, FINSEQ_1:def 7;
( q . j = <*j,(n -' j)*> & j <= n ) by A2, A4, A24, FINSEQ_1:1;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A22, A25; :: thesis: verum

end;

suppose j = n + 1 ; :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }

then (q ^ <*<*0,n*>*>) . j = <*0,n*> by A1, FINSEQ_1:42
.= <*0,(n -' 0)*> by NAT_D:40 ;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A22; :: thesis: verum

end;

end;

end;

hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } or x in rng (q ^ <*<*0,n*>*>) )
assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; :: thesis: x in rng (q ^ <*<*0,n*>*>)
then consider i being Element of NAT such that
A26: x = <*i,(n -' i)*> and
A27: i <= n ;
A28: ( i = 0 or i >= 0 + 1 ) by NAT_1:13;

now :: thesis: x in rng (q ^ <*<*0,n*>*>)

per cases ( i = 0 or i in Seg n ) by A27, A28, FINSEQ_1:1;

suppose A29: i = 0 ; :: thesis: x in rng (q ^ <*<*0,n*>*>)

A30: n + 1 in dom (q ^ <*<*0,n*>*>) by A6, FINSEQ_1:4;
(q ^ <*<*0,n*>*>) . (n + 1) = <*0,n*> by A1, FINSEQ_1:42
.= x by A26, A29, NAT_D:40 ;
hence x in rng (q ^ <*<*0,n*>*>) by A30, FUNCT_1:def 3; :: thesis: verum

end;

suppose A31: i in Seg n ; :: thesis: x in rng (q ^ <*<*0,n*>*>)

then q . i = x by A2, A4, A26;
then x in rng q by A3, A31, FUNCT_1:def 3;
hence x in rng (q ^ <*<*0,n*>*>) by A19; :: thesis: verum

end;

end;

end;

hence x in rng (q ^ <*<*0,n*>*>) ; :: thesis: verum

end;

consider A being finite Subset of (2 -tuples_on NAT) such that
A32: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
A33: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A34: A = { <*i,(n -' i)*> where i is Element of NAT : i <= n }

proof

thus A c= { <*i,(n -' i)*> where i is Element of NAT : i <= n } :: according to XBOOLE_0:def 10 :: thesis: { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } )
assume A35: x in A ; :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then reconsider p = x as Element of 2 -tuples_on NAT ;
consider d1, d2 being Element of NAT such that
A36: p = <*d1,d2*> by FINSEQ_2:100;
A37: d1 + d2 = Sum p by A36, RVSUM_1:77
.= n by A33, A35 ;
then n - d1 >= 0 ;
then A38: d2 = n -' d1 by A37, XREAL_0:def 2;
d1 <= n by A37, NAT_1:11;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A36, A38; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } or x in A )
assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; :: thesis: x in A
then consider i being Element of NAT such that
A39: x = <*i,(n -' i)*> and
A40: i <= n ;
A41: n - i >= 0 by A40, XREAL_1:48;
Sum <*i,(n -' i)*> = i + (n -' i) by RVSUM_1:77
.= i + (n - i) by A41, XREAL_0:def 2
.= n ;
hence x in A by A33, A39; :: thesis: verum

end;

field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 2 linearly_orders 2 -tuples_on NAT by ORDERS_1:37;
hence len (Decomp (n,2)) = n + 1 by A32, A34, A20, A18, ORDERS_1:38, PRE_POLY:11; :: thesis: verum