set f = { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ;
A1:
now for x, y1, y2 being object st [x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } holds
y1 = y2let x,
y1,
y2 be
object ;
( [x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies y1 = y2 )assume
[x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) }
;
( [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies y1 = y2 )then consider P19,
P29 being
Element of
Left_Cosets P such that A2:
[x,y1] = [P19,P29]
and A3:
ex
A1,
A2 being
Subset of
G ex
g being
Element of
G st
(
A2 = g * A1 &
A1 = P19 &
A2 = P29 &
g = h )
;
A4:
x = P19
by A2, XTUPLE_0:1;
assume
[x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) }
;
y1 = y2then consider P199,
P299 being
Element of
Left_Cosets P such that A5:
[x,y2] = [P199,P299]
and A6:
ex
A1,
A2 being
Subset of
G ex
g being
Element of
G st
(
A2 = g * A1 &
A1 = P199 &
A2 = P299 &
g = h )
;
x = P199
by A5, XTUPLE_0:1;
hence
y1 = y2
by A2, A3, A5, A6, A4, XTUPLE_0:1;
verum end;
now for x being object st x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } holds
ex y, z being object st x = [y,z]let x be
object ;
( x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies ex y, z being object st x = [y,z] )assume
x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) }
;
ex y, z being object st x = [y,z]then consider P1,
P2 being
Element of
Left_Cosets P such that A7:
x = [P1,P2]
and
ex
A1,
A2 being
Subset of
G ex
g being
Element of
G st
(
A2 = g * A1 &
A1 = P1 &
A2 = P2 &
g = h )
;
reconsider y =
P1,
z =
P2 as
object ;
take y =
y;
ex z being object st x = [y,z]take z =
z;
x = [y,z]thus
x = [y,z]
by A7;
verum end;
then reconsider f = { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;
then A12:
dom f = Left_Cosets P
by XTUPLE_0:def 12;
then
rng f c= Left_Cosets P
;
then reconsider f = f as Function of (Left_Cosets P),(Left_Cosets P) by A12, FUNCT_2:2;
take
f
; for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
thus
for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
verumproof
let P1 be
Element of
Left_Cosets P;
ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
set P2 =
f . P1;
not
Left_Cosets P is
empty
by GROUP_2:135;
then
[P1,(f . P1)] in f
by A12, FUNCT_1:1;
then consider P19,
P29 being
Element of
Left_Cosets P such that A16:
[P1,(f . P1)] = [P19,P29]
and A17:
ex
A1,
A2 being
Subset of
G ex
g being
Element of
G st
(
A2 = g * A1 &
A1 = P19 &
A2 = P29 &
h = g )
;
reconsider P2 =
f . P1 as
Element of
Left_Cosets P by A16, XTUPLE_0:1;
consider A1,
A2 being
Subset of
G,
g being
Element of
G such that A18:
(
A2 = g * A1 &
A1 = P19 )
and
A2 = P29
and A19:
h = g
by A17;
take
P2
;
ex A1, A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
take
A1
;
ex A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
take
A2
;
ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
take
g
;
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
thus
P2 = f . P1
;
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
thus
(
A2 = g * A1 &
A1 = P1 &
A2 = P2 &
g = h )
by A16, A17, A18, A19, XTUPLE_0:1;
verum
end;