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 ;
( 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:] )
;
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 A2, SUBSET_1:43;
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] )
;
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 BINOP_1:sch 1(A1);
now 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;
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;
for f being Vector of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]let f be
Vector of
F;
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 A5, XTUPLE_0:1;
hence
MLTGF . (
r,
[g,f])
= [(r * g),(r * f)]
by A5;
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)]
; verum