defpred S_{1}[ 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_{1}[a1,z,w]

A6: for a being Element of REAL

for z being Element of [: the carrier of X, the carrier of Y:] holds S_{1}[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_{1}[a,z,g . (a,z)]

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

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

proof

consider g being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] such that
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_{1}[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_{1}[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_{1}[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])]_{1}[a1,z,w]
; :: thesis: verum

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

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

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

hence
S
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;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

A6: for a being Element of REAL

for z being Element of [: the carrier of X, the carrier of Y:] holds S

A7: for a being Real

for z being Element of [: the carrier of X, the carrier of Y:] holds S

proof

take
g
; :: thesis: for a being Real
let a be Real; :: thesis: for z being Element of [: the carrier of X, the carrier of Y:] holds S_{1}[a,z,g . (a,z)]

let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: S_{1}[a,z,g . (a,z)]

reconsider a = a as Element of REAL by XREAL_0:def 1;

S_{1}[a,z,g . (a,z)]
by A6;

hence S_{1}[a,z,g . (a,z)]
; :: thesis: verum

end;let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: S

reconsider a = a as Element of REAL by XREAL_0:def 1;

S

hence S

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