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

( I is bijective & ( for x being Element of X holds I . x = <*x*> ) )

set CarrX = the carrier of X;

consider I being Function of the carrier of X,(product <* the carrier of X*>) such that

A1: ( I is one-to-one & I is onto & ( for x being object st x in the carrier of X holds

I . x = <*x*> ) ) by PRVECT_3:4;

len (carr <*X*>) = len <*X*> by PRVECT_1:def 11;

then A2: len (carr <*X*>) = 1 by FINSEQ_1:40;

A3: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

A4: <*X*> . 1 = X by FINSEQ_1:def 8;

1 in {1} by TARSKI:def 1;

then (carr <*X*>) . 1 = the carrier of X by A3, A4, PRVECT_1:def 11;

then A5: carr <*X*> = <* the carrier of X*> by A2, FINSEQ_1:40;

then reconsider I = I as Function of X,(product <*X*>) ;

for v, w being Element of X holds I . (v + w) = (I . v) + (I . w)

take I ; :: thesis: ( I is bijective & ( for x being Element of X holds I . x = <*x*> ) )

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

( I is bijective & ( for x being Element of X holds I . x = <*x*> ) )

set CarrX = the carrier of X;

consider I being Function of the carrier of X,(product <* the carrier of X*>) such that

A1: ( I is one-to-one & I is onto & ( for x being object st x in the carrier of X holds

I . x = <*x*> ) ) by PRVECT_3:4;

len (carr <*X*>) = len <*X*> by PRVECT_1:def 11;

then A2: len (carr <*X*>) = 1 by FINSEQ_1:40;

A3: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

A4: <*X*> . 1 = X by FINSEQ_1:def 8;

1 in {1} by TARSKI:def 1;

then (carr <*X*>) . 1 = the carrier of X by A3, A4, PRVECT_1:def 11;

then A5: carr <*X*> = <* the carrier of X*> by A2, FINSEQ_1:40;

then reconsider I = I as Function of X,(product <*X*>) ;

for v, w being Element of X holds I . (v + w) = (I . v) + (I . w)

proof

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

A6: ( I . v = <*v*> & I . w = <*w*> & I . (v + w) = <*(v + w)*> ) by A1;

A7: ( <*v*> . 1 = v & <*w*> . 1 = w ) by FINSEQ_1:40;

reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X*>) ;

1 in {1} by TARSKI:def 1;

then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;

A8: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_1:def 12;

A9: ([:(addop <*X*>):] . (Iv,Iw)) . j1 = ((addop <*X*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8

.= v + w by A8, A6, A7, FINSEQ_1:40 ;

consider Ivw being Function such that

A10: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being object st i in dom (carr <*X*>) holds

Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def 5;

A11: dom Ivw = Seg 1 by A2, A10, FINSEQ_1:def 3;

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

len Ivw = 1 by A11, FINSEQ_1:def 3;

hence I . (v + w) = (I . v) + (I . w) by A6, A10, A9, FINSEQ_1:40; :: thesis: verum

end;A6: ( I . v = <*v*> & I . w = <*w*> & I . (v + w) = <*(v + w)*> ) by A1;

A7: ( <*v*> . 1 = v & <*w*> . 1 = w ) by FINSEQ_1:40;

reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X*>) ;

1 in {1} by TARSKI:def 1;

then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;

A8: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_1:def 12;

A9: ([:(addop <*X*>):] . (Iv,Iw)) . j1 = ((addop <*X*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8

.= v + w by A8, A6, A7, FINSEQ_1:40 ;

consider Ivw being Function such that

A10: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being object st i in dom (carr <*X*>) holds

Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def 5;

A11: dom Ivw = Seg 1 by A2, A10, FINSEQ_1:def 3;

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

len Ivw = 1 by A11, FINSEQ_1:def 3;

hence I . (v + w) = (I . v) + (I . w) by A6, A10, A9, FINSEQ_1:40; :: thesis: verum

take I ; :: thesis: ( I is bijective & ( for x being Element of X holds I . x = <*x*> ) )

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