let X, Y be Group-Sequence; ex I being Homomorphism of (product <*(product X),(product Y)*>),(product (X ^ Y)) st
( I is bijective & ( for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) ) )
set PX = product X;
set PY = product Y;
set PXY = product (X ^ Y);
consider K being Homomorphism of [:(product X),(product Y):],(product (X ^ Y)) such that
A1:
( K is bijective & ( for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) ) )
by Th3;
consider J being Homomorphism of [:(product X),(product Y):],(product <*(product X),(product Y)*>) such that
A2:
( J is bijective & ( for x being Element of (product X)
for y being Element of (product Y) holds J . (x,y) = <*x,y*> ) )
by Th2;
reconsider JB = J " as Homomorphism of (product <*(product X),(product Y)*>),[:(product X),(product Y):] by A2, Th7;
dom J = the carrier of [:(product X),(product Y):]
by FUNCT_2:def 1;
then
rng JB = the carrier of [:(product X),(product Y):]
by A2, FUNCT_1:33;
then A3:
JB is onto
by FUNCT_2:def 3;
reconsider I = K * JB as Homomorphism of (product <*(product X),(product Y)*>),(product (X ^ Y)) ;
take
I
; ( I is bijective & ( for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) ) )
I is onto
by A1, A3, FUNCT_2:27;
hence
I is bijective
by A1, A2; for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 )
thus
for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 )
verumproof
let x be
Element of
(product X);
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 )let y be
Element of
(product Y);
ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 )
consider x1,
y1 being
FinSequence such that A4:
(
x = x1 &
y = y1 &
K . (
x,
y)
= x1 ^ y1 )
by A1;
A5:
J . (
x,
y)
= <*x,y*>
by A2;
[x,y] in the
carrier of
[:(product X),(product Y):]
;
then A6:
[x,y] in dom J
by FUNCT_2:def 1;
I . <*x,y*> = K . (JB . (J . [x,y]))
by A5, FUNCT_2:15;
then
I . <*x,y*> = x1 ^ y1
by A4, A6, A2, FUNCT_1:34;
hence
ex
x1,
y1 being
FinSequence st
(
x = x1 &
y = y1 &
I . <*x,y*> = x1 ^ y1 )
by A4;
verum
end;