let f be FinSequence of REAL ; :: thesis: ( 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) ) ) ; :: thesis: 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; :: thesis: ( i in dom ((a,b) Subnomial n) implies f . i = ((a,b) Subnomial n) . i )
assume B2: i in dom ((a,b) Subnomial n) ; :: thesis: 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; :: thesis: verum

end;

hence f = (a,b) Subnomial n by A4, FINSEQ_1:13; :: thesis: 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; :: thesis: verum