let f1, f2 be FinSequence of REAL ; :: thesis: ( dom p = dom f1 & ( for i being Nat st i in dom p holds
f1 . i = W . (p . i) ) & dom p = dom f2 & ( for i being Nat st i in dom p holds
f2 . i = W . (p . i) ) implies f1 = f2 )
assume that
A6: dom p = dom f1 and
A7: for i being Nat st i in dom p holds
f1 . i = W . (p . i) ; :: thesis: ( not dom p = dom f2 or ex i being Nat st
( i in dom p & not f2 . i = W . (p . i) ) or f1 = f2 )
assume that
A8: dom p = dom f2 and
A9: for i being Nat st i in dom p holds
f2 . i = W . (p . i) ; :: thesis: f1 = f2
now :: thesis: for i being Nat st i in dom f1 holds
f1 . i = f2 . i
let i be Nat; :: thesis: ( i in dom f1 implies f1 . i = f2 . i )
assume A10: i in dom f1 ; :: thesis: f1 . i = f2 . i
hence f1 . i = W . (p . i) by A6, A7
.= f2 . i by A6, A9, A10 ;
:: thesis: verum
end;
hence f1 = f2 by A6, A8; :: thesis: verum