let n be Element of NAT ; 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 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 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 = x2let x1,
x2 be
object ;
( 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
;
x1 = x2reconsider 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 x1 = x2per 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 A14:
(
x1 in Seg n &
x2 = n + 1 )
;
x1 = x2then 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;
verum end; suppose A16:
(
x1 = n + 1 &
x2 in Seg n )
;
x1 = x2then 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;
verum end; end; end; hence
x1 = x2
;
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 }
XBOOLE_0:def 10 { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= rng (q ^ <*<*0,n*>*>)
let x be
object ;
TARSKI:def 3 ( 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 }
;
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;
hence
x in rng (q ^ <*<*0,n*>*>)
;
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 }
XBOOLE_0:def 10 { <*i,(n -' i)*> where i is Element of NAT : i <= n } c= Aproof
let x be
object ;
TARSKI:def 3 ( not x in A or x in { <*i,(n -' i)*> where i is Element of NAT : i <= n } )
assume A35:
x in A
;
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;
verum
end;
let x be
object ;
TARSKI:def 3 ( 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 }
;
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;
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; verum