let f, g be FinSequence of L; :: thesis: ( len f = len E & ( for n being Nat st 1 <= n & n <= len f holds
f . n = ((B * E) . n) * (E /. n) ) & len g = len E & ( for n being Nat st 1 <= n & n <= len g holds
g . n = ((B * E) . n) * (E /. n) ) implies f = g )
assume that
A2: len f = len E and
A3: for n being Nat st 1 <= n & n <= len f holds
f . n = ((B * E) . n) * (E /. n) and
A4: len g = len E and
A5: for n being Nat st 1 <= n & n <= len g holds
g . n = ((B * E) . n) * (E /. n) ; :: thesis: f = g
thus len f = len g by A2, A4; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len f or f . b₁ = g . b₁ )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len f or f . n = g . n )
assume A6: ( 1 <= n & n <= len f ) ; :: thesis: f . n = g . n
hence f . n = ((B * E) . n) * (E /. n) by A3
.= g . n by A2, A4, A5, A6 ;
:: thesis: verum