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 A5: 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 A6: for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ; :: thesis: z1 = z2

A7: 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 x9 = x as Element of NAT by FUNCT_2:def 1;
thus z1 . x = (m1 . x9) * (m2 . x9) by A5
.= z2 . x by A6 ; :: thesis: verum

end;

dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1 ;
hence z1 = z2 by A7, FUNCT_1:2; :: thesis: verum