let n be Element of NAT ; :: thesis: len (Decomp (n,2)) = n + 1

deffunc H_{1}( 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_{1}(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;

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 }

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 }

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

deffunc H

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

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

then
q ^ <*<*0,n*>*> is one-to-one
by FUNCT_1:def 4;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;

end;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 = x2end;

hence
x1 = x2
; :: thesis: verumper 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;

end;

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;( 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

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;(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

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;(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

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

consider A being finite Subset of (2 -tuples_on NAT) such that
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*>*>)

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;

end;proof

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*>*>) )
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;

end;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 } end;

hence
x in { <*i,(n -' i)*> where i is Element of NAT : i <= n }
; :: thesis: verumper cases
( j in Seg n or j = n + 1 )
by A23, TARSKI:def 1;

end;

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;( 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

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*>*>)end;

hence
x in rng (q ^ <*<*0,n*>*>)
; :: thesis: verumper cases
( i = 0 or i in Seg n )
by A27, A28, FINSEQ_1:1;

end;

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

field (TuplesOrder 2) = 2 -tuples_on NAT
by ORDERS_1:15;
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

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;proof

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 )
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;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

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

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