let G be RealLinearSpace; :: thesis: ( ( for x being set holds
( x is Point of (product <*G*>) iff ex x1 being Point of G st x = <*x1*> ) ) & ( for x, y being Point of (product <*G*>)
for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*> ) & 0. (product <*G*>) = <*(0. G)*> & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) )
consider I being Function of G,(product <*G*>) such that
A1: ( I is one-to-one & I is onto & ( for x being Point of G holds
( I . x = <*x*> & ( for v, w being Point of G holds
( I . (v + w) = (I . v) + (I . w) & ( for v being Point of G
for r being Element of REAL holds
( I . (r * v) = r * (I . v) & 0. (product <*G*>) = I . (0. G) ) ) ) ) ) ) ) by PRVECT_3:11;
thus A2: for x being set holds
( x is Point of (product <*G*>) iff ex x1 being Point of G st x = <*x1*> ) :: thesis: ( ( for x, y being Point of (product <*G*>)
for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*> ) & 0. (product <*G*>) = <*(0. G)*> & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) )

proof

let y be set ; :: thesis: ( y is Point of (product <*G*>) iff ex x1 being Point of G st y = <*x1*> )

hereby :: thesis: ( ex x1 being Point of G st y = <*x1*> implies y is Point of (product <*G*>) )

assume y is Point of (product <*G*>) ; :: thesis: ex x being Element of the carrier of G st y = <*x*>
then consider x being Element of the carrier of G such that
A3: y = I . x by A1, FUNCT_2:113;
take x = x; :: thesis: y = <*x*>
thus y = <*x*> by A1, A3; :: thesis: verum

end;

now :: thesis: ( ex x1 being Point of G st y = <*x1*> implies y is Point of (product <*G*>) )

assume ex x1 being Point of G st y = <*x1*> ; :: thesis: y is Point of (product <*G*>)
then consider x1 being Point of G such that
A4: y = <*x1*> ;
I . x1 = <*x1*> by A1;
hence y is Point of (product <*G*>) by A4; :: thesis: verum

end;

hence ( ex x1 being Point of G st y = <*x1*> implies y is Point of (product <*G*>) ) ; :: thesis: verum

end;

thus A5: for x, y being Point of (product <*G*>)
for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*> :: thesis: ( 0. (product <*G*>) = <*(0. G)*> & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) )

proof

let x, y be Point of (product <*G*>); :: thesis: for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*>
let x1, y1 be Point of G; :: thesis: ( x = <*x1*> & y = <*y1*> implies x + y = <*(x1 + y1)*> )
assume A6: ( x = <*x1*> & y = <*y1*> ) ; :: thesis: x + y = <*(x1 + y1)*>
( I . (x1 + y1) = <*(x1 + y1)*> & I . x1 = <*x1*> & I . y1 = <*y1*> ) by A1;
hence <*(x1 + y1)*> = x + y by A1, A6; :: thesis: verum

end;

thus 0. (product <*G*>) = <*(0. G)*> by A1; :: thesis: ( ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) )
thus for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> :: thesis: for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*>

proof

let x be Point of (product <*G*>); :: thesis: for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*>
let x1 be Point of G; :: thesis: ( x = <*x1*> implies - x = <*(- x1)*> )
assume A7: x = <*x1*> ; :: thesis: - x = <*(- x1)*>
reconsider y = <*(- x1)*> as Point of (product <*G*>) by A2;
x + y = <*(x1 + (- x1))*> by A5, A7
.= <*(0. G)*> by RLVECT_1:def 10
.= 0. (product <*G*>) by A1 ;
hence - x = <*(- x1)*> by RLVECT_1:def 10; :: thesis: verum

end;

thus for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> :: thesis: verum

proof

let x be Point of (product <*G*>); :: thesis: for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*>
let x1 be Point of G; :: thesis: for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*>
let a be Real; :: thesis: ( x = <*x1*> implies a * x = <*(a * x1)*> )
assume A8: x = <*x1*> ; :: thesis: a * x = <*(a * x1)*>
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
A9: <*x1*> = I . x1 by A1;
I . (a0 * x1) = <*(a0 * x1)*> by A1;
hence a * x = <*(a * x1)*> by A1, A8, A9; :: thesis: verum

end;