let X, Y be AbGroup; :: thesis: ex I being Homomorphism of [:X,Y:],[:X,(product <*Y*>):] st

( I is bijective & ( for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )

consider J being Homomorphism of Y,(product <*Y*>) such that

A1: ( J is bijective & ( for y being Element of Y holds J . y = <*y*> ) ) by Th1;

defpred S_{1}[ object , object , object ] means $3 = [$1,<*$2*>];

A2: for x, y being object st x in the carrier of X & y in the carrier of Y holds

ex z being object st

( z in the carrier of [:X,(product <*Y*>):] & S_{1}[x,y,z] )

A4: for x, y being object st x in the carrier of X & y in the carrier of Y holds

S_{1}[x,y,I . (x,y)]
from BINOP_1:sch 1(A2);

reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;

for v, w being Element of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)

take I ; :: thesis: ( I is bijective & ( for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )

then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

hence I is bijective by A13; :: thesis: for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>]

thus for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>] by A4; :: thesis: verum

( I is bijective & ( for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )

consider J being Homomorphism of Y,(product <*Y*>) such that

A1: ( J is bijective & ( for y being Element of Y holds J . y = <*y*> ) ) by Th1;

defpred S

A2: for x, y being object st x in the carrier of X & y in the carrier of Y holds

ex z being object st

( z in the carrier of [:X,(product <*Y*>):] & S

proof

consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that
let x, y be object ; :: thesis: ( x in the carrier of X & y in the carrier of Y implies ex z being object st

( z in the carrier of [:X,(product <*Y*>):] & S_{1}[x,y,z] ) )

assume A3: ( x in the carrier of X & y in the carrier of Y ) ; :: thesis: ex z being object st

( z in the carrier of [:X,(product <*Y*>):] & S_{1}[x,y,z] )

then reconsider y0 = y as Element of Y ;

reconsider z = [x,<*y0*>] as set by TARSKI:1;

take z ; :: thesis: ( z in the carrier of [:X,(product <*Y*>):] & S_{1}[x,y,z] )

J . y0 = <*y0*> by A1;

hence ( z in the carrier of [:X,(product <*Y*>):] & S_{1}[x,y,z] )
by A3, ZFMISC_1:87; :: thesis: verum

end;( z in the carrier of [:X,(product <*Y*>):] & S

assume A3: ( x in the carrier of X & y in the carrier of Y ) ; :: thesis: ex z being object st

( z in the carrier of [:X,(product <*Y*>):] & S

then reconsider y0 = y as Element of Y ;

reconsider z = [x,<*y0*>] as set by TARSKI:1;

take z ; :: thesis: ( z in the carrier of [:X,(product <*Y*>):] & S

J . y0 = <*y0*> by A1;

hence ( z in the carrier of [:X,(product <*Y*>):] & S

A4: for x, y being object st x in the carrier of X & y in the carrier of Y holds

S

reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;

for v, w being Element of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)

proof

then reconsider I = I as Homomorphism of [:X,Y:],[:X,(product <*Y*>):] by VECTSP_1:def 20;
let v, w be Element of [:X,Y:]; :: thesis: I . (v + w) = (I . v) + (I . w)

consider x1 being Element of X, x2 being Element of Y such that

A5: v = [x1,x2] by SUBSET_1:43;

consider y1 being Element of X, y2 being Element of Y such that

A6: w = [y1,y2] by SUBSET_1:43;

A7: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A5, A6, PRVECT_3:def 1

.= [(x1 + y1),<*(x2 + y2)*>] by A4 ;

( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A5, A6;

then A8: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by A4;

A9: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by A1;

then reconsider xx2 = <*x2*> as Element of (product <*Y*>) ;

reconsider yy2 = <*y2*> as Element of (product <*Y*>) by A9;

<*(x2 + y2)*> = J . (x2 + y2) by A1

.= xx2 + yy2 by A9, VECTSP_1:def 20 ;

hence (I . v) + (I . w) = I . (v + w) by A7, A8, PRVECT_3:def 1; :: thesis: verum

end;consider x1 being Element of X, x2 being Element of Y such that

A5: v = [x1,x2] by SUBSET_1:43;

consider y1 being Element of X, y2 being Element of Y such that

A6: w = [y1,y2] by SUBSET_1:43;

A7: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A5, A6, PRVECT_3:def 1

.= [(x1 + y1),<*(x2 + y2)*>] by A4 ;

( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A5, A6;

then A8: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by A4;

A9: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by A1;

then reconsider xx2 = <*x2*> as Element of (product <*Y*>) ;

reconsider yy2 = <*y2*> as Element of (product <*Y*>) by A9;

<*(x2 + y2)*> = J . (x2 + y2) by A1

.= xx2 + yy2 by A9, VECTSP_1:def 20 ;

hence (I . v) + (I . w) = I . (v + w) by A7, A8, PRVECT_3:def 1; :: thesis: verum

take I ; :: thesis: ( I is bijective & ( for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )

now :: thesis: for z1, z2 being object st z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 holds

z1 = z2

then A13:
I is one-to-one
by FUNCT_2:19;z1 = z2

let z1, z2 be object ; :: thesis: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )

assume A10: ( 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 object such that

A11: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by A10, ZFMISC_1:def 2;

consider x2, y2 being object such that

A12: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by A10, ZFMISC_1:def 2;

[x1,<*y1*>] = I . (x1,y1) by A4, A11

.= I . (x2,y2) by A10, A11, A12

.= [x2,<*y2*>] by A4, A12 ;

then ( x1 = x2 & <*y1*> = <*y2*> ) by XTUPLE_0:1;

hence z1 = z2 by A11, A12, FINSEQ_1:76; :: thesis: verum

end;assume A10: ( 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 object such that

A11: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by A10, ZFMISC_1:def 2;

consider x2, y2 being object such that

A12: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by A10, ZFMISC_1:def 2;

[x1,<*y1*>] = I . (x1,y1) by A4, A11

.= I . (x2,y2) by A10, A11, A12

.= [x2,<*y2*>] by A4, A12 ;

then ( x1 = x2 & <*y1*> = <*y2*> ) by XTUPLE_0:1;

hence z1 = z2 by A11, A12, FINSEQ_1:76; :: thesis: verum

now :: thesis: for w being object st w in the carrier of [:X,(product <*Y*>):] holds

w in rng I

then
the carrier of [:X,(product <*Y*>):] c= rng I
by TARSKI:def 3;w in rng I

let w be object ; :: 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 object such that

A14: ( 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 A1, A14, FUNCT_2:def 3;

then consider y being object such that

A15: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:11;

reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by A14, A15, ZFMISC_1:87;

J . y = <*y*> by A15, A1;

then w = I . (x,y) by A4, A14, A15;

then w = I . z ;

hence w in rng I by FUNCT_2:4; :: thesis: verum

end;assume w in the carrier of [:X,(product <*Y*>):] ; :: thesis: w in rng I

then consider x, y1 being object such that

A14: ( 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 A1, A14, FUNCT_2:def 3;

then consider y being object such that

A15: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:11;

reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by A14, A15, ZFMISC_1:87;

J . y = <*y*> by A15, A1;

then w = I . (x,y) by A4, A14, A15;

then w = I . z ;

hence w in rng I by FUNCT_2:4; :: thesis: verum

then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

hence I is bijective by A13; :: thesis: for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>]

thus for x being Element of X

for y being Element of Y holds I . (x,y) = [x,<*y*>] by A4; :: thesis: verum