let f, g be FinSequence of V; :: thesis: ( len f = len x & ( for i being Nat st 1 <= i & i <= len x holds
f . i = (r /. i) * (x /. i) ) & len g = len x & ( for i being Nat st 1 <= i & i <= len x holds
g . i = (r /. i) * (x /. i) ) implies f = g )
assume that
A1: len f = len x and
A2: for i being Nat st 1 <= i & i <= len x holds
f . i = (r /. i) * (x /. i) and
A3: len g = len x and
A4: for i being Nat st 1 <= i & i <= len x holds
g . i = (r /. i) * (x /. i) ; :: thesis: f = g
thus len f = len g by A1, A3; :: 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 i be Nat; :: thesis: ( not 1 <= i or not i <= len f or f . i = g . i )
assume A5: ( 1 <= i & i <= len f ) ; :: thesis: f . i = g . i
thus f . i = (r /. i) * (x /. i) by A1, A2, A5
.= g . i by A1, A4, A5 ; :: thesis: verum