defpred S₁[ set , set ] means $2 = (m1 /. $1) * (m2 /. $1);
A1: for x being set st x in NAT holds
ex y being set st
( y in the carrier of L & S₁[x,y] ) ;
consider f being Function of NAT ,the carrier of L such that
A2: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
reconsider f = f as sequence of L ;
take f ; :: thesis: for i being Nat holds f . i = (m1 . i) * (m2 . i)

now

let i be Nat; :: thesis: f . i = (m1 . i) * (m2 . i)
A3: i in NAT by ORDINAL1:def 13;
dom m2 = NAT by FUNCT_2:def 1;
then A4: m2 /. i = m2 . i by A3, PARTFUN1:def 8;
dom m1 = NAT by FUNCT_2:def 1;
then m1 /. i = m1 . i by A3, PARTFUN1:def 8;
hence f . i = (m1 . i) * (m2 . i) by A2, A3, A4; :: thesis: verum

end;

hence for i being Nat holds f . i = (m1 . i) * (m2 . i) ; :: thesis: verum