let n, i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies (Decomp n,2) . i = <*(i -' 1),((n + 1) -' i)*> )
assume
i in Seg (n + 1)
; :: thesis: (Decomp n,2) . i = <*(i -' 1),((n + 1) -' i)*>
then A2:
( 1 <= i & i <= n + 1 )
by FINSEQ_1:3;
consider A being finite Subset of (2 -tuples_on NAT ) such that
A4:
Decomp n,2 = SgmX (TuplesOrder 2),A
and
A5:
for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n )
by Def4;
defpred S1[ Nat] means ( $1 <= n + 1 implies (Decomp n,2) . $1 = <*($1 -' 1),((n + 1) -' $1)*> );
A6:
S1[1]
A7:
for j being non empty Nat st S1[j] holds
S1[j + 1]
proof
let j be non
empty Nat;
:: thesis: ( S1[j] implies S1[j + 1] )
assume that A8:
(
j <= n + 1 implies
(Decomp n,2) . j = <*(j -' 1),((n + 1) -' j)*> )
and A9:
j + 1
<= n + 1
;
:: thesis: (Decomp n,2) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*>
A10:
j < n + 1
by A9, NAT_1:13;
j + 1
>= 1
by NAT_1:11;
then
j + 1
in Seg (n + 1)
by A9, FINSEQ_1:3;
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 8;
then consider d1,
d2 being
Element of
NAT such that A12:
(Decomp n,2) . (j + 1) = <*d1,d2*>
by FINSEQ_2:120;
field (TuplesOrder 2) = 2
-tuples_on NAT
by ORDERS_1:100;
then A13:
TuplesOrder 2
linearly_orders A
by ORDERS_1:133, ORDERS_1:134;
(Decomp n,2) . (j + 1) in rng (Decomp n,2)
by A11, FUNCT_1:def 5;
then
(Decomp n,2) . (j + 1) in A
by A4, A13, TRIANG_1:def 2;
then
Sum <*d1,d2*> = n
by A5, A12;
then A14:
d1 + d2 = n
by RVSUM_1:107;
then
n - d1 >= 0
;
then A15:
d2 = n -' d1
by A14, XREAL_0:def 2;
j >= 1
by NAT_1:14;
then A16:
j - 1
>= 1
- 1
by XREAL_1:11;
A17:
(n + 1) - j >= 0
by A10, XREAL_1:50;
then
n - (j - 1) >= 0
;
then A18:
n - (j -' 1) >= 0
by A16, XREAL_0:def 2;
n >= j
by A9, XREAL_1:8;
then A19:
n - j >= 0
by XREAL_1:50;
(n + 1) - (j + 1) >= 0
by A9, XREAL_1:50;
then A20:
(n + 1) -' (j + 1) =
n - j
by XREAL_0:def 2
.=
n -' j
by A19, XREAL_0:def 2
;
reconsider jj =
j as non
empty Element of
NAT by ORDINAL1:def 13;
(n + 1) -' j =
n - (j - 1)
by A17, XREAL_0:def 2
.=
n - (j -' 1)
by A16, XREAL_0:def 2
.=
n -' (j -' 1)
by A18, XREAL_0:def 2
;
then d1 =
(jj -' 1) + 1
by A8, A9, A12, A15, Th12, NAT_1:13
.=
j
by NAT_1:14, XREAL_1:237
;
hence
(Decomp n,2) . (j + 1) = <*((j + 1) -' 1),((n + 1) -' (j + 1))*>
by A12, A15, A20, NAT_D:34;
:: thesis: verum
end;
for j being non empty Nat holds S1[j]
from NAT_1:sch 10(A6, A7);
hence
(Decomp n,2) . i = <*(i -' 1),((n + 1) -' i)*>
by A2; :: thesis: verum