let E, F, G be RealLinearSpace; :: thesis: ( ( for x being set holds

( x is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = <*x1,x2,x3*> ) ) & ( for x1, y1 being Point of E

for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> ) & 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

A1: the carrier of [:E,F,G:] = [: the carrier of E, the carrier of F, the carrier of G:] ;

consider I being Function of [:E,F,G:],(product <*E,F,G*>) such that

A2: ( I is one-to-one & I is onto & ( for x being Point of E

for y being Point of F

for z being Point of G holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:E,F,G:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:E,F,G:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*E,F,G*>) = I . (0. [:E,F,G:]) ) by Th11;

thus for x being set holds

( x is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = <*x1,x2,x3*> ) :: thesis: ( ( for x1, y1 being Point of E

for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> ) & 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> :: thesis: ( 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> :: thesis: for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

let x2 be Point of F; :: thesis: for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

let x3 be Point of G; :: thesis: for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

let a be Real; :: thesis: a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

A14: <*x1,x2,x3*> = I . (x1,x2,x3) by A2;

I . (a * [x1,x2,x3]) = I . ((a * x1),(a * x2),(a * x3)) by Th8

.= <*(a * x1),(a * x2),(a * x3)*> by A2 ;

hence a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> by A2, A14; :: thesis: verum

( x is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = <*x1,x2,x3*> ) ) & ( for x1, y1 being Point of E

for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> ) & 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

A1: the carrier of [:E,F,G:] = [: the carrier of E, the carrier of F, the carrier of G:] ;

consider I being Function of [:E,F,G:],(product <*E,F,G*>) such that

A2: ( I is one-to-one & I is onto & ( for x being Point of E

for y being Point of F

for z being Point of G holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:E,F,G:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:E,F,G:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*E,F,G*>) = I . (0. [:E,F,G:]) ) by Th11;

thus for x being set holds

( x is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = <*x1,x2,x3*> ) :: thesis: ( ( for x1, y1 being Point of E

for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> ) & 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

proof

thus A8:
for x1, y1 being Point of E
let y be set ; :: thesis: ( y is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*> )

end;hereby :: thesis: ( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*> implies y is Point of (product <*E,F,G*>) )

thus
( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*> implies y is Point of (product <*E,F,G*>) )
; :: thesis: verumassume
y is Point of (product <*E,F,G*>)
; :: thesis: ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>

then y in the carrier of (product <*E,F,G*>) ;

then y in rng I by A2, FUNCT_2:def 3;

then consider x being Element of the carrier of [:E,F,G:] such that

A4: y = I . x by FUNCT_2:113;

consider x1 being Point of E, x2 being Point of F, x3 being Point of G such that

A5: x = [x1,x2,x3] by A1, Lm1;

take x1 = x1; :: thesis: ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>

take x2 = x2; :: thesis: ex x3 being Point of G st y = <*x1,x2,x3*>

take x3 = x3; :: thesis: y = <*x1,x2,x3*>

I . (x1,x2,x3) = <*x1,x2,x3*> by A2;

hence y = <*x1,x2,x3*> by A4, A5; :: thesis: verum

end;then y in the carrier of (product <*E,F,G*>) ;

then y in rng I by A2, FUNCT_2:def 3;

then consider x being Element of the carrier of [:E,F,G:] such that

A4: y = I . x by FUNCT_2:113;

consider x1 being Point of E, x2 being Point of F, x3 being Point of G such that

A5: x = [x1,x2,x3] by A1, Lm1;

take x1 = x1; :: thesis: ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>

take x2 = x2; :: thesis: ex x3 being Point of G st y = <*x1,x2,x3*>

take x3 = x3; :: thesis: y = <*x1,x2,x3*>

I . (x1,x2,x3) = <*x1,x2,x3*> by A2;

hence y = <*x1,x2,x3*> by A4, A5; :: thesis: verum

for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> :: thesis: ( 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

proof

thus A11:
0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*>
:: thesis: ( ( for x1 being Point of E
let x1, y1 be Point of E; :: thesis: for x2, y2 being Point of F

for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>

let x2, y2 be Point of F; :: thesis: for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>

let x3, y3 be Point of G; :: thesis: <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>

A10: [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by Th8;

( I . ((x1 + y1),(x2 + y2),(x3 + y3)) = <*(x1 + y1),(x2 + y2),(x3 + y3)*> & I . (x1,x2,x3) = <*x1,x2,x3*> & I . (y1,y2,y3) = <*y1,y2,y3*> ) by A2;

hence <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> by A2, A10; :: thesis: verum

end;for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>

let x2, y2 be Point of F; :: thesis: for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>

let x3, y3 be Point of G; :: thesis: <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>

A10: [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by Th8;

( I . ((x1 + y1),(x2 + y2),(x3 + y3)) = <*(x1 + y1),(x2 + y2),(x3 + y3)*> & I . (x1,x2,x3) = <*x1,x2,x3*> & I . (y1,y2,y3) = <*y1,y2,y3*> ) by A2;

hence <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> by A2, A10; :: thesis: verum

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )

proof

thus
for x1 being Point of E
I . ((0. E),(0. F),(0. G)) = <*(0. E),(0. F),(0. G)*>
by A2;

hence 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> by A2; :: thesis: verum

end;hence 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> by A2; :: thesis: verum

for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> :: thesis: for x1 being Point of E

for x2 being Point of F

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

proof

let x1 be Point of E; :: thesis: for x2 being Point of F
let x1 be Point of E; :: thesis: for x2 being Point of F

for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>

let x2 be Point of F; :: thesis: for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>

let x3 be Point of G; :: thesis: - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>

<*x1,x2,x3*> + <*(- x1),(- x2),(- x3)*> = <*(x1 + (- x1)),(x2 + (- x2)),(x3 + (- x3))*> by A8

.= <*(0. E),(x2 + (- x2)),(x3 + (- x3))*> by RLVECT_1:def 10

.= <*(0. E),(0. F),(x3 + (- x3))*> by RLVECT_1:def 10

.= 0. (product <*E,F,G*>) by A11, RLVECT_1:def 10 ;

hence - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> by RLVECT_1:def 10; :: thesis: verum

end;for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>

let x2 be Point of F; :: thesis: for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>

let x3 be Point of G; :: thesis: - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>

<*x1,x2,x3*> + <*(- x1),(- x2),(- x3)*> = <*(x1 + (- x1)),(x2 + (- x2)),(x3 + (- x3))*> by A8

.= <*(0. E),(x2 + (- x2)),(x3 + (- x3))*> by RLVECT_1:def 10

.= <*(0. E),(0. F),(x3 + (- x3))*> by RLVECT_1:def 10

.= 0. (product <*E,F,G*>) by A11, RLVECT_1:def 10 ;

hence - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> by RLVECT_1:def 10; :: thesis: verum

for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

let x2 be Point of F; :: thesis: for x3 being Point of G

for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

let x3 be Point of G; :: thesis: for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

let a be Real; :: thesis: a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>

A14: <*x1,x2,x3*> = I . (x1,x2,x3) by A2;

I . (a * [x1,x2,x3]) = I . ((a * x1),(a * x2),(a * x3)) by Th8

.= <*(a * x1),(a * x2),(a * x3)*> by A2 ;

hence a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> by A2, A14; :: thesis: verum