defpred S_{1}[ 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:] & S_{1}[x,y,z] )

A4: for x, y being object st x in the carrier of K & y in [: the carrier of G, the carrier of F:] holds

S_{1}[x,y,MLTGF . (x,y)]
from BINOP_1:sch 1(A1);

_{1} 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 b_{1} . (r,[g,f]) = [(r * g),(r * f)]
; :: thesis: verum

( 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:] & S

proof

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
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:] & S_{1}[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:] & S_{1}[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 A2, SUBSET_1:43;

set z = [(r * y1),(r * y2)];

( [(r * y1),(r * y2)] in [: the carrier of G, the carrier of F:] & S_{1}[x,y,[(r * y1),(r * y2)]] )
by A3;

hence ex z being object st

( z in [: the carrier of G, the carrier of F:] & S_{1}[x,y,z] )
; :: thesis: verum

end;( z in [: the carrier of G, the carrier of F:] & S

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:] & S

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 A2, SUBSET_1:43;

set z = [(r * y1),(r * y2)];

( [(r * y1),(r * y2)] in [: the carrier of G, the carrier of F:] & S

hence ex z being object st

( z in [: the carrier of G, the carrier of F:] & S

A4: for x, y being object st x in the carrier of K & y in [: the carrier of G, the carrier of F:] holds

S

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)]

hence
ex bfor 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)]

S_{1}[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 A5, XTUPLE_0:1;

hence MLTGF . (r,[g,f]) = [(r * g),(r * f)] by A5; :: thesis: verum

end;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)]

S

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 A5, XTUPLE_0:1;

hence MLTGF . (r,[g,f]) = [(r * g),(r * f)] by A5; :: thesis: verum

for r being Element of K

for g being Vector of G

for f being Vector of F holds b