let s be natural Number ; Newton_Coeff s = (1,1) In_Power s
A1:
for i being Nat st i in dom (Newton_Coeff s) holds
(Newton_Coeff s) . i = ((1,1) In_Power s) . i
proof
let i be
Nat;
( i in dom (Newton_Coeff s) implies (Newton_Coeff s) . i = ((1,1) In_Power s) . i )
assume A2:
i in dom (Newton_Coeff s)
;
(Newton_Coeff s) . i = ((1,1) In_Power s) . i
A3:
dom (Newton_Coeff s) =
Seg (len (Newton_Coeff s))
by FINSEQ_1:def 3
.=
Seg (s + 1)
by Def5
;
then
i >= 1
by A2, FINSEQ_1:1;
then reconsider m1 =
i - 1 as
Element of
NAT by INT_1:5;
i <= s + 1
by A2, A3, FINSEQ_1:1;
then
(s + 1) - 1
>= i - 1
by XREAL_1:9;
then reconsider l1 =
s - m1 as
Element of
NAT by INT_1:5;
dom (Newton_Coeff s) =
Seg (len ((1,1) In_Power s))
by A3, Def4
.=
dom ((1,1) In_Power s)
by FINSEQ_1:def 3
;
then ((1,1) In_Power s) . i =
((s choose m1) * (1 |^ l1)) * (1 |^ m1)
by A2, Def4
.=
(Newton_Coeff s) . i
by A2, Def5
;
hence
(Newton_Coeff s) . i = ((1,1) In_Power s) . i
;
verum
end;
len (Newton_Coeff s) =
s + 1
by Def5
.=
len ((1,1) In_Power s)
by Def4
;
hence
Newton_Coeff s = (1,1) In_Power s
by A1, FINSEQ_2:9; verum