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 FINSEQ_1:2, FINSEQ_1:def 3;

len <*X,Y*> = 2 by FINSEQ_1:44;

then A4: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

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 A4, A5, PRVECT_1:def 11;

then A6: carr <*X,Y*> = <* the carrier of X, the carrier of Y*> by A2, FINSEQ_1:44;

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)

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

( 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 FINSEQ_1:2, FINSEQ_1:def 3;

len <*X,Y*> = 2 by FINSEQ_1:44;

then A4: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

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 A4, A5, PRVECT_1:def 11;

then A6: carr <*X,Y*> = <* the carrier of X, the carrier of Y*> by A2, FINSEQ_1:44;

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

then reconsider I = I as Homomorphism of [:X,Y:],(product <*X,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, 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 A7, A8, PRVECT_3:def 1

.= <*(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 A3, TARSKI:def 2;

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 A12, A9, A11, FINSEQ_1:44 ;

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 A14, A9, A11, FINSEQ_1:44 ;

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 A2, A16, FINSEQ_1:def 3;

then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;

len Ivw = 2 by A17, FINSEQ_1:def 3;

hence I . (v + w) = (I . v) + (I . w) by A10, A16, A13, A15, FINSEQ_1:44; :: thesis: verum

end;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 A7, A8, PRVECT_3:def 1

.= <*(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 A3, TARSKI:def 2;

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 A12, A9, A11, FINSEQ_1:44 ;

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 A14, A9, A11, FINSEQ_1:44 ;

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 A2, A16, FINSEQ_1:def 3;

then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;

len Ivw = 2 by A17, FINSEQ_1:def 3;

hence I . (v + w) = (I . v) + (I . w) by A10, A16, A13, A15, FINSEQ_1:44; :: 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*> ) )

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