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)*> ) )

proof

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*> )

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*>) )

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

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: verum

end;

thus A8: 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)*> :: 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

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;

thus A11: 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> :: thesis: ( ( 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

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;

thus 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)*> :: 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
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;

let x1 be Point of E; :: thesis: 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)*>
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