let X be AbGroup; 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)
proof
let v,
w be
Element of
X;
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;
verum
end;
then reconsider I = I as Homomorphism of X,(product <*X*>) by VECTSP_1:def 20;
take
I
; ( 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; verum