defpred S₁[ set , set , set ] means for x being VECTOR of
for y being VECTOR of 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 x', y' being set such that
A2: x' in the carrier of X and
A3: y' in the carrier of Y and
A4: z = [x',y'] by ZFMISC_1:def 2;
reconsider y' = y' as VECTOR of by A3;
reconsider x' = x' as VECTOR of by A2;
reconsider w = [(the Mult of X . [a1,x']),(the Mult of Y . [a1,y'])] as Element of [:the carrier of X,the carrier of Y:] ;
take w ; :: thesis: S₁[a1,z,w]
for x being VECTOR of
for y being VECTOR of st z = [x,y] holds
w = [(the Mult of X . [a1,x]),(the Mult of Y . [a1,y])]

proof

let x be VECTOR of ; :: thesis: for y being VECTOR of st z = [x,y] holds
w = [(the Mult of X . [a1,x]),(the Mult of Y . [a1,y])]
let y be VECTOR of ; :: 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 = x' by A4, ZFMISC_1:33;
hence w = [(the Mult of X . [a1,x]),(the Mult of Y . [a1,y])] by A4, A5, ZFMISC_1:33; :: 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);
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
for y being VECTOR of 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
for y being VECTOR of 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
for y being VECTOR of 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
for y being VECTOR of st z = [x,y] holds
g . a,z = [(the Mult of X . [a,x]),(the Mult of Y . [a,y])] by A6; :: thesis: verum