let G, F be non empty RLSStruct ; :: thesis: ex MLTGF being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of REAL
for g being Point of G
for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
defpred S₁[ set , set , set ] means ex r being Element of REAL ex g being Point of G ex f being Point of F st
( r = $1 & $2 = [g,f] & $3 = [(r * g),(r * f)] );
set CarrG = the carrier of G;
set CarrF = the carrier of F;
P1: for x, y being set st x in REAL & y in [: the carrier of G, the carrier of F:] holds
ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in REAL & y in [: the carrier of G, the carrier of F:] implies ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] ) )
assume AS1: ( x in REAL & y in [: the carrier of G, the carrier of F:] ) ; :: thesis: ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] )
then reconsider r = x as Element of REAL ;
consider y1 being Point of G, y2 being Point of F such that
P2: y = [y1,y2] by AS1, LM01;
set z = [(r * y1),(r * y2)];
( [(r * y1),(r * y2)] in [: the carrier of G, the carrier of F:] & S₁[x,y,[(r * y1),(r * y2)]] ) by P2;
hence ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] ) ; :: thesis: verum

end;

consider MLTGF being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] such that
P2: for x, y being set st x in REAL & y in [: the carrier of G, the carrier of F:] holds
S₁[x,y,MLTGF . (x,y)] from BINOP_1:sch 1(P1);

now

let r be Element of REAL ; :: thesis: for g being Point of G
for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
let g be Point of G; :: thesis: for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
let f be Point of F; :: thesis: MLTGF . (r,[g,f]) = [(r * g),(r * f)]
S₁[r,[g,f],MLTGF . (r,[g,f])] by P2;
then consider rr being Element of REAL , gg being Point of G, ff being Point of F such that
P5: ( rr = r & [g,f] = [gg,ff] & MLTGF . (r,[g,f]) = [(rr * gg),(r * ff)] ) ;
( g = gg & f = ff ) by ZFMISC_1:33, P5;
hence MLTGF . (r,[g,f]) = [(r * g),(r * f)] by P5; :: thesis: verum

end;

hence ex MLTGF being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of REAL
for g being Point of G
for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)] ; :: thesis: verum