defpred S₁[ object , object , object ] means for x being VECTOR of X
for y being VECTOR of Y st $2 = [x,y] holds
$3 = [( the Mult of X . [$1,x]),( the Mult of Y . [$1,y])];
A1: for a1 being Element of REAL
for z being Element of [: the carrier of X, the carrier of Y:] ex w being Element of [: the carrier of X, the carrier of Y:] st S₁[a1,z,w]

proof

let a1 be Element of REAL ; :: thesis: for z being Element of [: the carrier of X, the carrier of Y:] ex w being Element of [: the carrier of X, the carrier of Y:] st S₁[a1,z,w]
let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: ex w being Element of [: the carrier of X, the carrier of Y:] st S₁[a1,z,w]
consider x9, y9 being object such that
A2: x9 in the carrier of X and
A3: y9 in the carrier of Y and
A4: z = [x9,y9] by ZFMISC_1:def 2;
reconsider y9 = y9 as VECTOR of Y by A3;
reconsider x9 = x9 as VECTOR of X by A2;
reconsider w = [( the Mult of X . [a1,x9]),( the Mult of Y . [a1,y9])] as Element of [: the carrier of X, the carrier of Y:] ;
take w ; :: thesis: S₁[a1,z,w]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])]

proof

let x be VECTOR of X; :: thesis: for y being VECTOR of Y st z = [x,y] holds
w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])]
let y be VECTOR of Y; :: thesis: ( z = [x,y] implies w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] )
assume A5: z = [x,y] ; :: thesis: w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])]
then x = x9 by A4, XTUPLE_0:1;
hence w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] by A4, A5, XTUPLE_0:1; :: thesis: verum

end;

hence S₁[a1,z,w] ; :: thesis: verum

end;

consider g being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] such that
A6: for a being Element of REAL
for z being Element of [: the carrier of X, the carrier of Y:] holds S₁[a,z,g . (a,z)] from BINOP_1:sch 3(A1);
A7: for a being Real
for z being Element of [: the carrier of X, the carrier of Y:] holds S₁[a,z,g . (a,z)]

proof

let a be Real; :: thesis: for z being Element of [: the carrier of X, the carrier of Y:] holds S₁[a,z,g . (a,z)]
let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: S₁[a,z,g . (a,z)]
reconsider a = a as Element of REAL by XREAL_0:def 1;
S₁[a,z,g . (a,z)] by A6;
hence S₁[a,z,g . (a,z)] ; :: thesis: verum

end;

take g ; :: thesis: for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
let a be Real; :: thesis: for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
thus for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] by A7; :: thesis: verum