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₁[ 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₁[j] holds
S₁[j + 1]

proof

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₁[j] implies S₁[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;

A17: S₁[1]

proof

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;

for j being non zero Nat holds S₁[j] from NAT_1:sch 10(A17, A4);
hence (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> by A1; :: thesis: verum