let X, Y be AbGroup; :: thesis: ex I being Homomorphism of [:X,Y:],(product <*X,Y*>) st
( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = <*x,y*> ) )

set CarrX = the carrier of X;
set CarrY = the carrier of Y;
consider I being Function of [: the carrier of X, the carrier of Y:],(product <* the carrier of X, the carrier of Y*>) such that
A1: ( I is one-to-one & I is onto & ( for x, y being object st x in the carrier of X & y in the carrier of Y holds
I . (x,y) = <*x,y*> ) ) by PRVECT_3:5;
len (carr <*X,Y*>) = len <*X,Y*> by PRVECT_1:def 11;
then A2: len (carr <*X,Y*>) = 2 by FINSEQ_1:44;
then A3: dom (carr <*X,Y*>) = {1,2} by ;
len <*X,Y*> = 2 by FINSEQ_1:44;
then A4: dom <*X,Y*> = {1,2} by ;
A5: ( <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:44;
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then ( (carr <*X,Y*>) . 1 = the carrier of X & (carr <*X,Y*>) . 2 = the carrier of Y ) by ;
then A6: carr <*X,Y*> = <* the carrier of X, the carrier of Y*> by ;
then reconsider I = I as Function of [:X,Y:],(product <*X,Y*>) ;
for v, w being Element of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)
proof
let v, w be Element of [:X,Y:]; :: thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Element of X, y1 being Element of Y such that
A7: v = [x1,y1] by SUBSET_1:43;
consider x2 being Element of X, y2 being Element of Y such that
A8: w = [x2,y2] by SUBSET_1:43;
( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A7, A8;
then A9: ( I . v = <*x1,y1*> & I . w = <*x2,y2*> ) by A1;
A10: I . (v + w) = I . ((x1 + x2),(y1 + y2)) by
.= <*(x1 + x2),(y1 + y2)*> by A1 ;
A11: ( <*x1,y1*> . 1 = x1 & <*x2,y2*> . 1 = x2 & <*x1,y1*> . 2 = y1 & <*x2,y2*> . 2 = y2 ) by FINSEQ_1:44;
reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X,Y*>) ;
reconsider j1 = 1, j2 = 2 as Element of dom (carr <*X,Y*>) by ;
A12: (addop <*X,Y*>) . j1 = the addF of (<*X,Y*> . j1) by PRVECT_1:def 12;
A13: ([:(addop <*X,Y*>):] . (Iv,Iw)) . j1 = ((addop <*X,Y*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8
.= x1 + x2 by ;
A14: (addop <*X,Y*>) . j2 = the addF of (<*X,Y*> . j2) by PRVECT_1:def 12;
A15: ([:(addop <*X,Y*>):] . (Iv,Iw)) . j2 = ((addop <*X,Y*>) . j2) . ((Iv . j2),(Iw . j2)) by PRVECT_1:def 8
.= y1 + y2 by ;
consider Ivw being Function such that
A16: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X,Y*>) & ( for i being object st i in dom (carr <*X,Y*>) holds
Ivw . i in (carr <*X,Y*>) . i ) ) by CARD_3:def 5;
A17: dom Ivw = Seg 2 by ;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by ;
hence I . (v + w) = (I . v) + (I . w) by ; :: thesis: verum
end;
then reconsider I = I as Homomorphism of [:X,Y:],(product <*X,Y*>) by VECTSP_1:def 20;
take I ; :: thesis: ( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = <*x,y*> ) )

thus ( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = <*x,y*> ) ) by A1, A6; :: thesis: verum