let X be AbGroup; :: thesis: ex I being Homomorphism of 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 () = len <*X*> by PRVECT_1:def 11;
then A2: len () = 1 by FINSEQ_1:40;
A3: dom <*X*> = {1} by ;
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 ;
then A5: carr <*X*> = <* the carrier of X*> by ;
then reconsider I = I as Function of X,() ;
for v, w being Element of X holds I . (v + w) = (I . v) + (I . w)
proof
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 () ;
1 in {1} by TARSKI:def 1;
then reconsider j1 = 1 as Element of dom () by ;
A8: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_1:def 12;
A9: ([:():] . (Iv,Iw)) . j1 = (() . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8
.= v + w by ;
consider Ivw being Function such that
A10: ( (I . v) + (I . w) = Ivw & dom Ivw = dom () & ( for i being object st i in dom () holds
Ivw . i in () . i ) ) by CARD_3:def 5;
A11: dom Ivw = Seg 1 by ;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by ;
hence I . (v + w) = (I . v) + (I . w) by ; :: thesis: verum
end;
then reconsider I = I as Homomorphism of X,() by VECTSP_1:def 20;
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