let n, i be Element of NAT ; ( 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)
; (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 S1[j] holds
S1[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;
( 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
;
(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;
verum
end;
A17:
S1[1]
for j being non zero Nat holds S1[j]
from NAT_1:sch 10(A17, A4);
hence
(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>
by A1; verum