let f be FinSequence of REAL ; ( f = (a,b) Subnomial n iff ( len f = n + 1 & ( for i, l, m being Nat st i in dom f & m = i - 1 & l = n - m holds
f . i = (a |^ l) * (b |^ m) ) ) )
L1: len ((a,b) Subnomial n) =
len ((a,b) Subnomial ((n + 1) - 1))
.=
n + 1
;
L2:
( len f = len ((a,b) Subnomial n) iff dom f = dom ((a,b) Subnomial n) )
by FINSEQ_3:29;
( len f = len ((a,b) Subnomial n) & ( for i, l, m being Nat st i in dom ((a,b) Subnomial n) & m = i - 1 & l = n - m holds
f . i = (a |^ l) * (b |^ m) ) implies f = (a,b) Subnomial n )
proof
assume A3:
(
len f = len ((a,b) Subnomial n) & ( for
i,
l,
m being
Nat st
i in dom ((a,b) Subnomial n) &
m = i - 1 &
l = n - m holds
f . i = (a |^ l) * (b |^ m) ) )
;
f = (a,b) Subnomial n
A4:
(
dom f = dom ((a,b) Subnomial n) & ( for
i,
l,
m being
Nat st
i in dom ((a,b) Subnomial n) &
m = i - 1 &
l = n - m holds
f . i = (a |^ l) * (b |^ m) ) )
by A3, FINSEQ_3:29;
for
i being
Nat st
i in dom ((a,b) Subnomial n) holds
f . i = ((a,b) Subnomial n) . i
proof
let i be
Nat;
( i in dom ((a,b) Subnomial n) implies f . i = ((a,b) Subnomial n) . i )
assume B2:
i in dom ((a,b) Subnomial n)
;
f . i = ((a,b) Subnomial n) . i
reconsider m =
i - 1 as
Nat by B2, FINSEQ_3:26;
len ((a,b) Subnomial ((n + 1) - 1)) = n + 1
;
then
(n + 1) - (m + 1) is
Element of
NAT
by FINSEQ_3:26, B2;
then reconsider l =
n - m as
Nat ;
f . i = (a |^ l) * (b |^ m)
by A3, B2;
hence
f . i = ((a,b) Subnomial n) . i
by LmS1, B2;
verum
end;
hence
f = (
a,
b)
Subnomial n
by A4, FINSEQ_1:13;
verum
end;
hence
( f = (a,b) Subnomial n iff ( len f = n + 1 & ( for i, l, m being Nat st i in dom f & m = i - 1 & l = n - m holds
f . i = (a |^ l) * (b |^ m) ) ) )
by L1, L2, LmS1; verum