defpred S1[ 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 S1[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 S1[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 S1[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: S1[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 ;
hence w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] by ; :: thesis: verum
end;
hence S1[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 S1[a,z,g . (a,z)] from A7: for a being Real
for z being Element of [: the carrier of X, the carrier of Y:] holds S1[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 S1[a,z,g . (a,z)]
let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: S1[a,z,g . (a,z)]
reconsider a = a as Element of REAL by XREAL_0:def 1;
S1[a,z,g . (a,z)] by A6;
hence S1[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