let a, b be Real; for n being Nat holds (a,b) Subnomial n = Rev ((b,a) Subnomial n)
let n be Nat; (a,b) Subnomial n = Rev ((b,a) Subnomial n)
A1:
( dom ((a,b) Subnomial n) = dom (Newton_Coeff n) & dom ((b,a) Subnomial n) = dom (Newton_Coeff n) )
by DOMN;
then A2:
dom ((a,b) Subnomial n) = dom (Rev ((b,a) Subnomial n))
by FINSEQ_5:57;
for i being object st i in dom ((a,b) Subnomial n) holds
((a,b) Subnomial n) . i = (Rev ((b,a) Subnomial n)) . i
proof
let i be
object ;
( i in dom ((a,b) Subnomial n) implies ((a,b) Subnomial n) . i = (Rev ((b,a) Subnomial n)) . i )
assume B1:
i in dom ((a,b) Subnomial n)
;
((a,b) Subnomial n) . i = (Rev ((b,a) Subnomial n)) . i
reconsider i =
i as
Nat by B1;
reconsider m =
i - 1 as
Nat by B1, FINSEQ_3:26;
(len ((a,b) Subnomial ((n + 1) - 1))) - (m + 1) is
Element of
NAT
by B1, FINSEQ_3:26;
then reconsider l =
n - m as
Nat ;
set k =
l + 1;
B2:
i in dom (Rev ((b,a) Subnomial ((n + 1) - 1)))
by A1, FINSEQ_5:57, B1;
(l + 1) + i =
(len ((b,a) Subnomial ((n + 1) - 1))) + 1
.=
(len (Rev ((b,a) Subnomial ((n + 1) - 1)))) + 1
by FINSEQ_5:def 3
;
then B3:
l + 1
in dom (Rev (Rev ((b,a) Subnomial ((n + 1) - 1))))
by B2, FINSEQ_5:59;
B4:
l = (l + 1) - 1
;
B5:
m = n - l
;
((a,b) Subnomial n) . i =
(a |^ l) * (b |^ m)
by B1, Def2
.=
((b,a) Subnomial n) . (((len ((b,a) Subnomial ((n + 1) - 1))) - i) + 1)
by B3, B4, B5, Def2
.=
(Rev ((b,a) Subnomial n)) . i
by FINSEQ_5:58, A1, B1
;
hence
((a,b) Subnomial n) . i = (Rev ((b,a) Subnomial n)) . i
;
verum
end;
hence
(a,b) Subnomial n = Rev ((b,a) Subnomial n)
by A2, FUNCT_1:2; verum