let G, F be RealNormSpace; :: thesis:
consider I being Function of [:G,F:],(product <*G,F*>) such that
AS: ( I is one-to-one & I is onto & ( for x being Point of G
for y being Point of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:G,F:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) & ( for v being Point of [:G,F:] holds ||.(I . v).|| = ||.v.|| ) ) by ThHOM02;
thus X1: for x being set holds
( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) :: thesis:

let y be set ; :: thesis:

assume y is Point of (product <*G,F*>) ; :: thesis:
then y in the carrier of (product <*G,F*>) ;
then y in rng I by AS, FUNCT_2:def 3;
then consider x being Element of the carrier of [:G,F:] such that
X11: y = I . x by FUNCT_2:190;
consider x1 being Point of G, x2 being Point of F such that
X12: x = [x1,x2] by LM01;
take x1 = x1; :: thesis:
take x2 = x2; :: thesis:
I . (x1,x2) = <*x1,x2*> by AS;
hence y = <*x1,x2*> by X11, X12; :: thesis:

end;

assume ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ; :: thesis:
then consider x1 being Point of G, x2 being Point of F such that
X21: y = <*x1,x2*> ;
X22: I . [x1,x2] in rng I by FUNCT_2:189;
I . (x1,x2) = <*x1,x2*> by AS;
hence y is Point of (product <*G,F*>) by X21, X22; :: thesis:

end;

thus X2: for x, y being Point of (product <*G,F*>)
for x1, y1 being Point of G
for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> :: thesis:

let x, y be Point of (product <*G,F*>); :: thesis:
let x1, y1 be Point of G; :: thesis:
let x2, y2 be Point of F; :: thesis:
assume B3: ( x = <*x1,x2*> & y = <*y1,y2*> ) ; :: thesis:
reconsider z = [x1,x2], w = [y1,y2] as Point of [:G,F:] ;
X0: z + w = [(x1 + y1),(x2 + y2)] by defADD;
X1: I . ((x1 + y1),(x2 + y2)) = <*(x1 + y1),(x2 + y2)*> by AS;
( I . (x1,x2) = <*x1,x2*> & I . (y1,y2) = <*y1,y2*> ) by AS;
hence <*(x1 + y1),(x2 + y2)*> = x + y by AS, X0, X1, B3; :: thesis:

end;

I . ((0. G),(0. F)) = <*(0. G),(0. F)*> by AS;
hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by AS; :: thesis:

end;

thus for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> :: thesis:

let x be Point of (product <*G,F*>); :: thesis:
let x1 be Point of G; :: thesis:
let x2 be Point of F; :: thesis:
assume B3: x = <*x1,x2*> ; :: thesis:
reconsider y = <*(- x1),(- x2)*> as Point of (product <*G,F*>) by X1;
x + y = <*(x1 + (- x1)),(x2 + (- x2))*> by X2, B3
.= <*(0. G),(x2 + (- x2))*> by RLVECT_1:def 13
.= 0. (product <*G,F*>) by X3, RLVECT_1:def 13 ;
hence - x = <*(- x1),(- x2)*> by RLVECT_1:def 13; :: thesis:

end;

thus for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> :: thesis:

let x be Point of (product <*G,F*>); :: thesis:
let x1 be Point of G; :: thesis:
let x2 be Point of F; :: thesis:
let a be real number ; :: thesis:
assume B3: x = <*x1,x2*> ; :: thesis:
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
reconsider y = [x1,x2] as Point of [:G,F:] ;
Y1: <*x1,x2*> = I . (x1,x2) by AS;
I . (a * y) = I . ((a0 * x1),(a0 * x2)) by ThZ03
.= <*(a0 * x1),(a0 * x2)*> by AS ;
hence a * x = <*(a * x1),(a * x2)*> by B3, Y1, AS; :: thesis:

end;

thus for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) :: thesis:

let x be Point of (product <*G,F*>); :: thesis:
let x1 be Point of G; :: thesis:
let x2 be Point of F; :: thesis:
assume B3: x = <*x1,x2*> ; :: thesis:
reconsider y = [x1,x2] as Point of [:G,F:] ;
consider w being Element of REAL 2 such that
Y1: ( w = <*||.x1.||,||.x2.||*> & ||.y.|| = |.w.| ) by ThZ03;
take w ; :: thesis:
Y2: I . y = I . (x1,x2)
.= x by AS, B3 ;
thus w = <*||.x1.||,||.x2.||*> by Y1; :: thesis:
thus ||.x.|| = |.w.| by AS, Y1, Y2; :: thesis:

end;