let n, i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> )

defpred S_{1}[ Nat] means ( $1 <= n + 1 implies (Decomp (n,2)) . $1 = <*($1 -' 1),((n + 1) -' $1)*> );

assume i in Seg (n + 1) ; :: thesis: (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>

then A1: ( 1 <= i & i <= n + 1 ) by FINSEQ_1:1;

consider A being finite Subset of (2 -tuples_on NAT) such that

A2: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and

A3: for p being Element of 2 -tuples_on NAT holds

( p in A iff Sum p = n ) by Def4;

A4: for j being non zero Nat st S_{1}[j] holds

S_{1}[j + 1]
_{1}[1]
_{1}[j]
from NAT_1:sch 10(A17, A4);

hence (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> by A1; :: thesis: verum

defpred S

assume i in Seg (n + 1) ; :: thesis: (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>

then A1: ( 1 <= i & i <= n + 1 ) by FINSEQ_1:1;

consider A being finite Subset of (2 -tuples_on NAT) such that

A2: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and

A3: for p being Element of 2 -tuples_on NAT holds

( p in A iff Sum p = n ) by Def4;

A4: for j being non zero Nat st S

S

proof

A17:
S
field (TuplesOrder 2) = 2 -tuples_on NAT
by ORDERS_1:15;

then A5: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;

let j be non zero Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume that

A6: ( j <= n + 1 implies (Decomp (n,2)) . j = <*(j -' 1),((n + 1) -' j)*> ) and

A7: j + 1 <= n + 1 ; :: thesis: (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*>

n >= j by A7, XREAL_1:6;

then A8: n - j >= 0 by XREAL_1:48;

(n + 1) - (j + 1) >= 0 by A7, XREAL_1:48;

then A9: (n + 1) -' (j + 1) = n - j by XREAL_0:def 2

.= n -' j by A8, XREAL_0:def 2 ;

reconsider jj = j as non zero Element of NAT by ORDINAL1:def 12;

j >= 1 by NAT_1:14;

then A10: j - 1 >= 1 - 1 by XREAL_1:9;

j + 1 >= 1 by NAT_1:11;

then j + 1 in Seg (n + 1) by A7, FINSEQ_1:1;

then j + 1 in Seg (len (Decomp (n,2))) by Th9;

then A11: j + 1 in dom (Decomp (n,2)) by FINSEQ_1:def 3;

then (Decomp (n,2)) . (j + 1) = (Decomp (n,2)) /. (j + 1) by PARTFUN1:def 6;

then consider d1, d2 being Element of NAT such that

A12: (Decomp (n,2)) . (j + 1) = <*d1,d2*> by FINSEQ_2:100;

(Decomp (n,2)) . (j + 1) in rng (Decomp (n,2)) by A11, FUNCT_1:def 3;

then (Decomp (n,2)) . (j + 1) in A by A2, A5, PRE_POLY:def 2;

then Sum <*d1,d2*> = n by A3, A12;

then A13: d1 + d2 = n by RVSUM_1:77;

then n - d1 >= 0 ;

then A14: d2 = n -' d1 by A13, XREAL_0:def 2;

j < n + 1 by A7, NAT_1:13;

then A15: (n + 1) - j >= 0 by XREAL_1:48;

then n - (j - 1) >= 0 ;

then A16: n - (j -' 1) >= 0 by A10, XREAL_0:def 2;

(n + 1) -' j = n - (j - 1) by A15, XREAL_0:def 2

.= n - (j -' 1) by A10, XREAL_0:def 2

.= n -' (j -' 1) by A16, XREAL_0:def 2 ;

then d1 = (jj -' 1) + 1 by A6, A7, A12, A14, Th12, NAT_1:13

.= j by NAT_1:14, XREAL_1:235 ;

hence (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*> by A12, A14, A9, NAT_D:34; :: thesis: verum

end;then A5: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;

let j be non zero Nat; :: thesis: ( S

assume that

A6: ( j <= n + 1 implies (Decomp (n,2)) . j = <*(j -' 1),((n + 1) -' j)*> ) and

A7: j + 1 <= n + 1 ; :: thesis: (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*>

n >= j by A7, XREAL_1:6;

then A8: n - j >= 0 by XREAL_1:48;

(n + 1) - (j + 1) >= 0 by A7, XREAL_1:48;

then A9: (n + 1) -' (j + 1) = n - j by XREAL_0:def 2

.= n -' j by A8, XREAL_0:def 2 ;

reconsider jj = j as non zero Element of NAT by ORDINAL1:def 12;

j >= 1 by NAT_1:14;

then A10: j - 1 >= 1 - 1 by XREAL_1:9;

j + 1 >= 1 by NAT_1:11;

then j + 1 in Seg (n + 1) by A7, FINSEQ_1:1;

then j + 1 in Seg (len (Decomp (n,2))) by Th9;

then A11: j + 1 in dom (Decomp (n,2)) by FINSEQ_1:def 3;

then (Decomp (n,2)) . (j + 1) = (Decomp (n,2)) /. (j + 1) by PARTFUN1:def 6;

then consider d1, d2 being Element of NAT such that

A12: (Decomp (n,2)) . (j + 1) = <*d1,d2*> by FINSEQ_2:100;

(Decomp (n,2)) . (j + 1) in rng (Decomp (n,2)) by A11, FUNCT_1:def 3;

then (Decomp (n,2)) . (j + 1) in A by A2, A5, PRE_POLY:def 2;

then Sum <*d1,d2*> = n by A3, A12;

then A13: d1 + d2 = n by RVSUM_1:77;

then n - d1 >= 0 ;

then A14: d2 = n -' d1 by A13, XREAL_0:def 2;

j < n + 1 by A7, NAT_1:13;

then A15: (n + 1) - j >= 0 by XREAL_1:48;

then n - (j - 1) >= 0 ;

then A16: n - (j -' 1) >= 0 by A10, XREAL_0:def 2;

(n + 1) -' j = n - (j - 1) by A15, XREAL_0:def 2

.= n - (j -' 1) by A10, XREAL_0:def 2

.= n -' (j -' 1) by A16, XREAL_0:def 2 ;

then d1 = (jj -' 1) + 1 by A6, A7, A12, A14, Th12, NAT_1:13

.= j by NAT_1:14, XREAL_1:235 ;

hence (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*> by A12, A14, A9, NAT_D:34; :: thesis: verum

proof

for j being non zero Nat holds S
assume
1 <= n + 1
; :: thesis: (Decomp (n,2)) . 1 = <*(1 -' 1),((n + 1) -' 1)*>

thus (Decomp (n,2)) . 1 = <*0,n*> by Th13

.= <*(1 -' 1),n*> by XREAL_1:232

.= <*(1 -' 1),((n + 1) -' 1)*> by NAT_D:34 ; :: thesis: verum

end;thus (Decomp (n,2)) . 1 = <*0,n*> by Th13

.= <*(1 -' 1),n*> by XREAL_1:232

.= <*(1 -' 1),((n + 1) -' 1)*> by NAT_D:34 ; :: thesis: verum

hence (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> by A1; :: thesis: verum