let n be Element of NAT ; :: thesis: len (Decomp (n,2)) = n + 1
deffunc H1( 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 = H1(k) from A3: dom q = Seg n by ;
set q1 = q ^ ;
A4: dom q = Seg n by ;
A5: len (q ^ ) = n + 1 by ;
then A6: dom (q ^ ) = Seg (n + 1) by FINSEQ_1:def 3;
now :: thesis: for x1, x2 being object st x1 in dom (q ^ ) & x2 in dom (q ^ ) & (q ^ ) . x1 = (q ^ ) . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom (q ^ ) & x2 in dom (q ^ ) & (q ^ ) . x1 = (q ^ ) . x2 implies x1 = x2 )
assume that
A7: x1 in dom (q ^ ) and
A8: x2 in dom (q ^ ) and
A9: (q ^ ) . x1 = (q ^ ) . x2 ; :: thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A7, A8;
x2 in (Seg n) \/ {(n + 1)} by ;
then A10: ( x2 in Seg n or x2 in {(n + 1)} ) by XBOOLE_0:def 3;
x1 in (Seg n) \/ {(n + 1)} by ;
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 ;
suppose A12: ( x1 in Seg n & x2 in Seg n ) ; :: thesis: x1 = x2
then A13: ( (q ^ ) . k1 = q . k1 & (q ^ ) . k2 = q . k2 ) by ;
( q . k1 = <*k1,(n -' k1)*> & q . k2 = <*k2,(n -' k2)*> ) by A2, A4, A12;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A14: ( x1 in Seg n & x2 = n + 1 ) ; :: thesis: x1 = x2
then A15: (q ^ ) . k2 = <*0,n*> by ;
(q ^ ) . k1 = q . k1 by
.= <*k1,(n -' k1)*> by A2, A4, A14 ;
then k1 = 0 by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A16: ( x1 = n + 1 & x2 in Seg n ) ; :: thesis: x1 = x2
then A17: (q ^ ) . k1 = <*0,n*> by ;
(q ^ ) . k2 = q . k2 by
.= <*k2,(n -' k2)*> by A2, A4, A16 ;
then k2 = 0 by ;
hence x1 = x2 by ; :: 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 ^ is one-to-one by FUNCT_1:def 4;
then A18: card (rng (q ^ )) = n + 1 by ;
A19: rng q c= rng (q ^ ) by FINSEQ_1:29;
A20: rng (q ^ ) = { <*i,(n -' i)*> where i is Element of NAT : i <= n }
proof
thus rng (q ^ ) 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 ^ )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (q ^ ) or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } )
assume x in rng (q ^ ) ; :: 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 ^ ) and
A22: (q ^ ) . j = x by FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
j in (Seg n) \/ {(n + 1)} by ;
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 ;
suppose A24: j in Seg n ; :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then A25: (q ^ ) . j = q . j by ;
( q . j = <*j,(n -' j)*> & j <= n ) by ;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by ; :: thesis: verum
end;
suppose j = n + 1 ; :: thesis: x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
then (q ^ ) . j = <*0,n*> by
.= <*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 ^ ) )
assume x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } ; :: thesis: x in rng (q ^ )
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 ^ )
per cases ( i = 0 or i in Seg n ) by ;
suppose A29: i = 0 ; :: thesis: x in rng (q ^ )
A30: n + 1 in dom (q ^ ) by ;
(q ^ ) . (n + 1) = <*0,n*> by
.= x by ;
hence x in rng (q ^ ) by ; :: thesis: verum
end;
suppose A31: i in Seg n ; :: thesis: x in rng (q ^ )
then q . i = x by A2, A4, A26;
then x in rng q by ;
hence x in rng (q ^ ) by A19; :: thesis: verum
end;
end;
end;
hence x in rng (q ^ ) ; :: thesis: verum
end;
consider A being finite Subset of () such that
A32: Decomp (n,2) = SgmX ((),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
.= n by ;
then n - d1 >= 0 ;
then A38: d2 = n -' d1 by ;
d1 <= n by ;
hence x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } by ; :: 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 ;
Sum <*i,(n -' i)*> = i + (n -' i) by RVSUM_1:77
.= i + (n - i) by
.= n ;
hence x in A by ; :: thesis: verum
end;
field () = 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 ; :: thesis: verum