let p1, p2 be sequence of L; :: thesis: ( ( for n being Element of NAT holds p1 . n = v * (p . n) ) & ( for n being Element of NAT holds p2 . n = v * (p . n) ) implies p1 = p2 )
assume that
A2: for n being Element of NAT holds p1 . n = v * (p . n) and
A3: for n being Element of NAT holds p2 . n = v * (p . n) ; :: thesis: p1 = p2

now :: thesis: for k being Element of NAT holds p1 . k = p2 . k

let k be Element of NAT ; :: thesis: p1 . k = p2 . k
thus p1 . k = v * (p . k) by A2
.= p2 . k by A3 ; :: thesis: verum

end;

hence p1 = p2 by FUNCT_2:63; :: thesis: verum