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