let X, Y be non empty RealLinearSpace; :: thesis: ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )
consider J being Function of Y,(product <*Y*>) such that
P0: ( J is one-to-one & J is onto & ( for y being Point of Y holds J . y = <*y*> ) & ( for v, w being Point of Y holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of Y
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. Y) = 0. (product <*Y*>) ) by ThHOM01AA;
defpred S₁[ set , set , set ] means $3 = [$1,<*$2*>];
R1: for x, y being set st x in the carrier of X & y in the carrier of Y holds
ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in the carrier of X & y in the carrier of Y implies ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S₁[x,y,z] ) )
assume AS0: ( x in the carrier of X & y in the carrier of Y ) ; :: thesis: ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S₁[x,y,z] )
then reconsider y0 = y as Point of Y ;
J . y0 = <*y0*> by P0;
then [x,<*y*>] in [: the carrier of X, the carrier of (product <*Y*>):] by ZFMISC_1:106, AS0;
hence ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S₁[x,y,z] ) ; :: thesis: verum

end;

consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that
R2: for x, y being set st x in the carrier of X & y in the carrier of Y holds
S₁[x,y,I . (x,y)] from BINOP_1:sch 1(R1);
reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;
take I ; :: thesis: ( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )

now

let z1, z2 be set ; :: thesis: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )
assume P3: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
consider x1, y1 being set such that
P4: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by ZFMISC_1:def 2, P3;
consider x2, y2 being set such that
P5: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by ZFMISC_1:def 2, P3;
[x1,<*y1*>] = I . (x1,y1) by R2, P4
.= I . (x2,y2) by P3, P4, P5
.= [x2,<*y2*>] by R2, P5 ;
then ( x1 = x2 & <*y1*> = <*y2*> ) by ZFMISC_1:33;
hence z1 = z2 by P4, P5, FINSEQ_1:97; :: thesis: verum

end;

hence I is one-to-one by FUNCT_2:25; :: thesis: ( I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )

now

let w be set ; :: thesis: ( w in the carrier of [:X,(product <*Y*>):] implies w in rng I )
assume w in the carrier of [:X,(product <*Y*>):] ; :: thesis: w in rng I
then consider x, y1 being set such that
P4: ( x in the carrier of X & y1 in the carrier of (product <*Y*>) & w = [x,y1] ) by ZFMISC_1:def 2;
y1 in rng J by FUNCT_2:def 3, P0, P4;
then consider y being set such that
P5: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:17;
reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by P4, P5, ZFMISC_1:106;
J . y = <*y*> by P5, P0;
then w = I . (x,y) by R2, P4, P5;
then w = I . z ;
hence w in rng I by FUNCT_2:6; :: thesis: verum

end;

then the carrier of [:X,(product <*Y*>):] c= rng I by TARSKI:def 3;
then the carrier of [:X,(product <*Y*>):] = rng I by XBOOLE_0:def 10;
hence I is onto by FUNCT_2:def 3; :: thesis: ( ( for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )
thus for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] by R2; :: thesis: ( ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )
thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) :: thesis: ( ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )

proof

let v, w be Point of [:X,Y:]; :: thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Point of X, x2 being Point of Y such that
A1: v = [x1,x2] by LM01;
consider y1 being Point of X, y2 being Point of Y such that
A2: w = [y1,y2] by LM01;
A4: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A1, A2, defADD
.= [(x1 + y1),<*(x2 + y2)*>] by R2 ;
( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A1, A2;
then A5: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by R2;
A7: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by P0;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
reconsider yy2 = <*y2*> as Point of (product <*Y*>) by A7;
<*(x2 + y2)*> = J . (x2 + y2) by P0
.= xx2 + yy2 by A7, P0 ;
hence (I . v) + (I . w) = I . (v + w) by A4, A5, defADD; :: thesis: verum

end;

thus for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) :: thesis: I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):]

proof

let v be Point of [:X,Y:]; :: thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; :: thesis: I . (r * v) = r * (I . v)
consider x1 being Point of X, x2 being Point of Y such that
A1: v = [x1,x2] by LM01;
A4: I . (r * v) = I . ((r * x1),(r * x2)) by A1, ThZ02
.= [(r * x1),<*(r * x2)*>] by R2 ;
A5: I . v = I . (x1,x2) by A1
.= [x1,<*x2*>] by R2 ;
A7: J . x2 = <*x2*> by P0;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
<*(r * x2)*> = J . (r * x2) by P0
.= r * xx2 by A7, P0 ;
hence r * (I . v) = I . (r * v) by A4, A5, ThZ02; :: thesis: verum

end;

A9: <*(0. Y)*> = 0. (product <*Y*>) by P0;
I . (0. [:X,Y:]) = I . ((0. X),(0. Y)) ;
hence I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] by A9, R2; :: thesis: verum