let n, i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> )
defpred S1[ 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 () such that
A2: Decomp (n,2) = SgmX ((),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 S1[j] holds
S1[j + 1]
proof
field () = 2 -tuples_on NAT by ORDERS_1:15;
then A5: TuplesOrder 2 linearly_orders A by ;
let j be non zero Nat; :: thesis: ( S1[j] implies S1[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 ;
then A8: n - j >= 0 by XREAL_1:48;
(n + 1) - (j + 1) >= 0 by ;
then A9: (n + 1) -' (j + 1) = n - j by XREAL_0:def 2
.= n -' j by ;
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 ;
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 ;
then (Decomp (n,2)) . (j + 1) in A by ;
then Sum <*d1,d2*> = n by ;
then A13: d1 + d2 = n by RVSUM_1:77;
then n - d1 >= 0 ;
then A14: d2 = n -' d1 by ;
j < n + 1 by ;
then A15: (n + 1) - j >= 0 by XREAL_1:48;
then n - (j - 1) >= 0 ;
then A16: n - (j -' 1) >= 0 by ;
(n + 1) -' j = n - (j - 1) by
.= n - (j -' 1) by
.= n -' (j -' 1) by ;
then d1 = (jj -' 1) + 1 by
.= j by ;
hence (Decomp (n,2)) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*> by ; :: thesis: verum
end;
A17: S1[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 S1[j] from hence (Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*> by A1; :: thesis: verum