let n be Element of NAT ; :: thesis: len (Decomp n,2) = n + 1
consider A being finite Subset of (2 -tuples_on NAT ) such that
A1: Decomp n,2 = SgmX (TuplesOrder 2),A and
A2: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A3: 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 set ; :: 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 A4: 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
A5: p = <*d1,d2*> by FINSEQ_2:120;
A6: d1 + d2 = Sum p by A5, RVSUM_1:107
.= n by A2, A4 ;
then A7: d1 <= n by NAT_1:11;
n - d1 >= 0 by A6;
then d2 = n -' d1 by A6, XREAL_0:def 2;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A5, A7; :: thesis: verum

end;

let x be set ; :: 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
A8: x = <*i,(n -' i)*> and
A9: i <= n ;
A10: n - i >= 0 by A9, XREAL_1:50;
Sum <*i,(n -' i)*> = i + (n -' i) by RVSUM_1:107
.= i + (n - i) by A10, XREAL_0:def 2
.= n ;
hence x in A by A2, A8; :: thesis: verum

end;

deffunc H₁( Nat) -> set = <*$1,(n -' $1)*>;
consider q being FinSequence such that
A11: len q = n and
A12: for k being Nat st k in dom q holds
q . k = H₁(k) from FINSEQ_1:sch 2();
A13: dom q = Seg n by A11, FINSEQ_1:def 3;
set q1 = q ^ <*<*0 ,n*>*>;
A14: rng q c= rng (q ^ <*<*0 ,n*>*>) by FINSEQ_1:42;
A15: len (q ^ <*<*0 ,n*>*>) = n + 1 by A11, FINSEQ_2:19;
then A16: dom (q ^ <*<*0 ,n*>*>) = Seg (n + 1) by FINSEQ_1:def 3;
A17: dom q = Seg n by A11, FINSEQ_1:def 3;
A18: 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 set ; :: 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
A19: j in dom (q ^ <*<*0 ,n*>*>) and
A20: (q ^ <*<*0 ,n*>*>) . j = x by FINSEQ_2:11;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j in (Seg n) \/ {(n + 1)} by A16, A19, FINSEQ_1:11;
then A21: ( j in Seg n or j in {(n + 1)} ) by XBOOLE_0:def 3;

now

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

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

then A23: q . j = <*j,(n -' j)*> by A12, A13;
A24: j <= n by A22, FINSEQ_1:3;
(q ^ <*<*0 ,n*>*>) . j = q . j by A17, A22, FINSEQ_1:def 7;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A20, A23, A24; :: 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 A11, FINSEQ_1:59
.= <*0 ,(n -' 0 )*> by NAT_D:40 ;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by A20; :: 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 set ; :: 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
A25: x = <*i,(n -' i)*> and
A26: i <= n ;
A27: ( i = 0 or i >= 0 + 1 ) by NAT_1:13;

now

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

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

A29: n + 1 in dom (q ^ <*<*0 ,n*>*>) by A16, FINSEQ_1:6;
(q ^ <*<*0 ,n*>*>) . (n + 1) = <*0 ,n*> by A11, FINSEQ_1:59
.= x by A25, A28, NAT_D:40 ;
hence x in rng (q ^ <*<*0 ,n*>*>) by A29, FUNCT_1:def 5; :: thesis: verum

end;

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

then q . i = x by A12, A25, A13;
then x in rng q by A17, A30, FUNCT_1:def 5;
hence x in rng (q ^ <*<*0 ,n*>*>) by A14; :: thesis: verum

end;

end;

end;

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

end;

now

let x1, x2 be set ; :: 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
A31: x1 in dom (q ^ <*<*0 ,n*>*>) and
A32: x2 in dom (q ^ <*<*0 ,n*>*>) and
A33: (q ^ <*<*0 ,n*>*>) . x1 = (q ^ <*<*0 ,n*>*>) . x2 ; :: thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A31, A32;
( x1 in (Seg n) \/ {(n + 1)} & x2 in (Seg n) \/ {(n + 1)} ) by A16, A31, A32, FINSEQ_1:11;
then A34: ( ( x1 in Seg n or x1 in {(n + 1)} ) & ( x2 in Seg n or x2 in {(n + 1)} ) ) by XBOOLE_0:def 3;

now

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 A34, TARSKI:def 1;

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

then A36: ( (q ^ <*<*0 ,n*>*>) . k1 = q . k1 & (q ^ <*<*0 ,n*>*>) . k2 = q . k2 ) by A17, FINSEQ_1:def 7;
( q . k1 = <*k1,(n -' k1)*> & q . k2 = <*k2,(n -' k2)*> ) by A12, A35, A13;
hence x1 = x2 by A33, A36, GROUP_7:2; :: thesis: verum

end;

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

then A38: (q ^ <*<*0 ,n*>*>) . k1 = q . k1 by A17, FINSEQ_1:def 7
.= <*k1,(n -' k1)*> by A12, A37, A13 ;
(q ^ <*<*0 ,n*>*>) . k2 = <*0 ,n*> by A11, A37, FINSEQ_1:59;
then k1 = 0 by A33, A38, GROUP_7:2;
hence x1 = x2 by A37, FINSEQ_1:3; :: thesis: verum

end;

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

then A40: (q ^ <*<*0 ,n*>*>) . k2 = q . k2 by A17, FINSEQ_1:def 7
.= <*k2,(n -' k2)*> by A12, A39, A13 ;
(q ^ <*<*0 ,n*>*>) . k1 = <*0 ,n*> by A11, A39, FINSEQ_1:59;
then k2 = 0 by A33, A40, GROUP_7:2;
hence x1 = x2 by A39, FINSEQ_1:3; :: 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 8;
then A41: card (rng (q ^ <*<*0 ,n*>*>)) = n + 1 by A15, FINSEQ_4:77;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:100;
then TuplesOrder 2 linearly_orders 2 -tuples_on NAT by ORDERS_1:133;
hence len (Decomp n,2) = n + 1 by A1, A3, A18, A41, ORDERS_1:134, TRIANG_1:9; :: thesis: verum