let z1, z2 be sequence of L; :: thesis: ( ( for i being Nat holds z1 . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ) implies z1 = z2 )
assume A4: for i being Nat holds z1 . i = (m1 . i) * (m2 . i) ; :: thesis: ( ex i being Nat st not z2 . i = (m1 . i) * (m2 . i) or z1 = z2 )
assume A5: for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ; :: thesis: z1 = z2
A6: dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1 ;

now

let x be set ; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume x in dom z1 ; :: thesis: z1 . x = z2 . x
then reconsider x' = x as Element of NAT by FUNCT_2:def 1;
thus z1 . x = (m1 . x') * (m2 . x') by A4
.= z2 . x by A5 ; :: thesis: verum

end;

hence z1 = z2 by A6, FUNCT_1:9; :: thesis: verum