defpred S1[ object , object , object ] means ex r being Element of the carrier of K ex g being Vector of G ex f being Vector 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;
A1: for x, y being object st x in the carrier of K & y in [: the carrier of G, the carrier of F:] holds
ex z being object st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] )
proof
let x, y be object ; :: thesis: ( x in the carrier of K & y in [: the carrier of G, the carrier of F:] implies ex z being object st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) )

assume A2: ( x in the carrier of K & y in [: the carrier of G, the carrier of F:] ) ; :: thesis: ex z being object st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] )

then reconsider r = x as Element of the carrier of K ;
consider y1 being Vector of G, y2 being Vector of F such that
A3: y = [y1,y2] by ;
set z = [(r * y1),(r * y2)];
( [(r * y1),(r * y2)] in [: the carrier of G, the carrier of F:] & S1[x,y,[(r * y1),(r * y2)]] ) by A3;
hence ex z being object st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ; :: thesis: verum
end;
consider MLTGF being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] such that
A4: for x, y being object st x in the carrier of K & y in [: the carrier of G, the carrier of F:] holds
S1[x,y,MLTGF . (x,y)] from
now :: thesis: for r being Element of K
for g being Vector of G
for f being Vector of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
let r be Element of K; :: thesis: for g being Vector of G
for f being Vector of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]

let g be Vector of G; :: thesis: for f being Vector of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
let f be Vector of F; :: thesis: MLTGF . (r,[g,f]) = [(r * g),(r * f)]
S1[r,[g,f],MLTGF . (r,[g,f])] by A4;
then consider rr being Element of the carrier of K, gg being Vector of G, ff being Vector of F such that
A5: ( rr = r & [g,f] = [gg,ff] & MLTGF . (r,[g,f]) = [(rr * gg),(r * ff)] ) ;
( g = gg & f = ff ) by ;
hence MLTGF . (r,[g,f]) = [(r * g),(r * f)] by A5; :: thesis: verum
end;
hence ex b1 being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of K
for g being Vector of G
for f being Vector of F holds b1 . (r,[g,f]) = [(r * g),(r * f)] ; :: thesis: verum