A1: now :: thesis: ( not O is empty implies ex IT being Action of O,(Cosets N) st

for o being Element of O holds IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } )

for o being Element of O holds IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } )

deffunc H_{1}( object ) -> set = { [A,B] where A, B is Element of Cosets N : for o being Element of O st $1 = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ;

reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;

assume A2: not O is empty ; :: thesis: ex IT being Action of O,(Cosets N) st

for o being Element of O holds IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

A3: Cosets N = Cosets H by Def14;

for x being object st x in O holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A4);

then consider IT being Function of O,(Funcs ((Cosets N),(Cosets N))) such that

A33: for x being object st x in O holds

IT . x = H_{1}(x)
;

reconsider IT = IT as Action of O,(Cosets N) ;

take IT = IT; :: thesis: for o being Element of O holds IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

let o be Element of O; :: thesis: IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

reconsider x = o as set ;

set X = { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ;

set Y = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ;

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A2, A33;

hence IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A34, TARSKI:2; :: thesis: verum

end;ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ;

reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;

assume A2: not O is empty ; :: thesis: ex IT being Action of O,(Cosets N) st

for o being Element of O holds IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

A3: Cosets N = Cosets H by Def14;

A4: now :: thesis: for x being object st x in O holds

H_{1}(x) in Funcs ((Cosets N),(Cosets N))

ex f being Function of O,(Funcs ((Cosets N),(Cosets N))) st H

let x be object ; :: thesis: ( x in O implies H_{1}(x) in Funcs ((Cosets N),(Cosets N)) )

set f = H_{1}(x);

_{1}(x) in Funcs ((Cosets N),(Cosets N))

_{1}(x) as Function by A5, FUNCT_1:def 1, RELAT_1:def 1;

hence H_{1}(x) in Funcs ((Cosets N),(Cosets N))
by A30, FUNCT_2:def 2; :: thesis: verum

end;set f = H

A5: now :: thesis: for y being object st y in H_{1}(x) holds

ex A, B being object st y = [A,B]

assume A7:
x in O
; :: thesis: Hex A, B being object st y = [A,B]

let y be object ; :: thesis: ( y in H_{1}(x) implies ex A, B being object st y = [A,B] )

assume y in H_{1}(x)
; :: thesis: ex A, B being object st y = [A,B]

then consider A, B being Element of Cosets N such that

A6: y = [A,B] and

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) ;

reconsider A = A, B = B as object ;

take A = A; :: thesis: ex B being object st y = [A,B]

take B = B; :: thesis: y = [A,B]

thus y = [A,B] by A6; :: thesis: verum

end;assume y in H

then consider A, B being Element of Cosets N such that

A6: y = [A,B] and

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) ;

reconsider A = A, B = B as object ;

take A = A; :: thesis: ex B being object st y = [A,B]

take B = B; :: thesis: y = [A,B]

thus y = [A,B] by A6; :: thesis: verum

now :: thesis: for y, y1, y2 being object st [y,y1] in H_{1}(x) & [y,y2] in H_{1}(x) holds

y1 = y2

then reconsider f = Hy1 = y2

reconsider o = x as Element of O by A7;

let y, y1, y2 be object ; :: thesis: ( [y,y1] in H_{1}(x) & [y,y2] in H_{1}(x) implies y1 = y2 )

assume [y,y1] in H_{1}(x)
; :: thesis: ( [y,y2] in H_{1}(x) implies y1 = y2 )

then consider A1, B1 being Element of Cosets N such that

A8: [y,y1] = [A1,B1] and

A9: for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A1 & h in B1 & h = (G ^ o) . g ) ;

assume [y,y2] in H_{1}(x)
; :: thesis: y1 = y2

then consider A2, B2 being Element of Cosets N such that

A10: [y,y2] = [A2,B2] and

A11: for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A2 & h in B2 & h = (G ^ o) . g ) ;

A12: y1 = B1 by A8, XTUPLE_0:1;

A13: y2 = B2 by A10, XTUPLE_0:1;

A14: y = A2 by A10, XTUPLE_0:1;

set f = G ^ o;

A15: y = A1 by A8, XTUPLE_0:1;

consider g1, h1 being Element of G such that

A16: g1 in A1 and

A17: h1 in B1 and

A18: h1 = (G ^ o) . g1 by A9;

consider g2, h2 being Element of G such that

A19: g2 in A2 and

A20: h2 in B2 and

A21: h2 = (G ^ o) . g2 by A11;

reconsider A1 = A1, A2 = A2, B1 = B1, B2 = B2 as Element of Cosets H by Def14;

A22: A2 = g2 * H by A19, Lm8;

A1 = g1 * H by A16, Lm8;

then (g2 ") * g1 in H by A15, A14, A22, GROUP_2:114;

then (g2 ") * g1 in the carrier of H by STRUCT_0:def 5;

then (g2 ") * g1 in N by STRUCT_0:def 5;

then (G ^ o) . ((g2 ") * g1) in N by Lm9;

then ((G ^ o) . (g2 ")) * ((G ^ o) . g1) in N by GROUP_6:def 6;

then (h2 ") * h1 in N by A18, A21, GROUP_6:32;

then (h2 ") * h1 in the carrier of N by STRUCT_0:def 5;

then A23: (h2 ") * h1 in H by STRUCT_0:def 5;

A24: B2 = h2 * H by A20, Lm8;

B1 = h1 * H by A17, Lm8;

hence y1 = y2 by A12, A13, A23, A24, GROUP_2:114; :: thesis: verum

end;let y, y1, y2 be object ; :: thesis: ( [y,y1] in H

assume [y,y1] in H

then consider A1, B1 being Element of Cosets N such that

A8: [y,y1] = [A1,B1] and

A9: for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A1 & h in B1 & h = (G ^ o) . g ) ;

assume [y,y2] in H

then consider A2, B2 being Element of Cosets N such that

A10: [y,y2] = [A2,B2] and

A11: for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A2 & h in B2 & h = (G ^ o) . g ) ;

A12: y1 = B1 by A8, XTUPLE_0:1;

A13: y2 = B2 by A10, XTUPLE_0:1;

A14: y = A2 by A10, XTUPLE_0:1;

set f = G ^ o;

A15: y = A1 by A8, XTUPLE_0:1;

consider g1, h1 being Element of G such that

A16: g1 in A1 and

A17: h1 in B1 and

A18: h1 = (G ^ o) . g1 by A9;

consider g2, h2 being Element of G such that

A19: g2 in A2 and

A20: h2 in B2 and

A21: h2 = (G ^ o) . g2 by A11;

reconsider A1 = A1, A2 = A2, B1 = B1, B2 = B2 as Element of Cosets H by Def14;

A22: A2 = g2 * H by A19, Lm8;

A1 = g1 * H by A16, Lm8;

then (g2 ") * g1 in H by A15, A14, A22, GROUP_2:114;

then (g2 ") * g1 in the carrier of H by STRUCT_0:def 5;

then (g2 ") * g1 in N by STRUCT_0:def 5;

then (G ^ o) . ((g2 ") * g1) in N by Lm9;

then ((G ^ o) . (g2 ")) * ((G ^ o) . g1) in N by GROUP_6:def 6;

then (h2 ") * h1 in N by A18, A21, GROUP_6:32;

then (h2 ") * h1 in the carrier of N by STRUCT_0:def 5;

then A23: (h2 ") * h1 in H by STRUCT_0:def 5;

A24: B2 = h2 * H by A20, Lm8;

B1 = h1 * H by A17, Lm8;

hence y1 = y2 by A12, A13, A23, A24, GROUP_2:114; :: thesis: verum

now :: thesis: for y1 being object holds

( ( y1 in Cosets N implies ex y2 being object st [y1,y2] in f ) & ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N ) )

then A30:
dom f = Cosets N
by XTUPLE_0:def 12;( ( y1 in Cosets N implies ex y2 being object st [y1,y2] in f ) & ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N ) )

let y1 be object ; :: thesis: ( ( y1 in Cosets N implies ex y2 being object st [y1,y2] in f ) & ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N ) )

consider A, B being Element of Cosets N such that

A29: [y1,y2] = [A,B] and

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A28;

A in Cosets N by A3;

hence y1 in Cosets N by A29, XTUPLE_0:1; :: thesis: verum

end;hereby :: thesis: ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N )

given y2 being object such that A28:
[y1,y2] in f
; :: thesis: y1 in Cosets Nreconsider o = x as Element of O by A7;

assume A25: y1 in Cosets N ; :: thesis: ex y2 being object st [y1,y2] in f

then reconsider A = y1 as Element of Cosets N ;

y1 in Cosets H by A25, Def14;

then consider g being Element of G such that

A26: y1 = g * H and

y1 = H * g by GROUP_6:13;

set h = (G ^ o) . g;

reconsider B = ((G ^ o) . g) * H as Element of Cosets N by A3, GROUP_2:def 15;

reconsider y2 = B as object ;

take y2 = y2; :: thesis: [y1,y2] in f

end;assume A25: y1 in Cosets N ; :: thesis: ex y2 being object st [y1,y2] in f

then reconsider A = y1 as Element of Cosets N ;

y1 in Cosets H by A25, Def14;

then consider g being Element of G such that

A26: y1 = g * H and

y1 = H * g by GROUP_6:13;

set h = (G ^ o) . g;

reconsider B = ((G ^ o) . g) * H as Element of Cosets N by A3, GROUP_2:def 15;

reconsider y2 = B as object ;

take y2 = y2; :: thesis: [y1,y2] in f

now :: thesis: for o being Element of O st x = o holds

ex g being Element of G ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g )

hence
[y1,y2] in f
; :: thesis: verumex g being Element of G ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g )

let o be Element of O; :: thesis: ( x = o implies ex g being Element of G ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g ) )

assume A27: x = o ; :: thesis: ex g being Element of G ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g )

take g = g; :: thesis: ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g )

take h = (G ^ o) . g; :: thesis: ( g in A & h in B & h = (G ^ o) . g )

thus g in A by A3, A26, Lm8; :: thesis: ( h in B & h = (G ^ o) . g )

thus h in B by A3, Lm8; :: thesis: h = (G ^ o) . g

thus h = (G ^ o) . g by A27; :: thesis: verum

end;( g in A & h in B & h = (G ^ o) . g ) )

assume A27: x = o ; :: thesis: ex g being Element of G ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g )

take g = g; :: thesis: ex h being Element of the carrier of G st

( g in A & h in B & h = (G ^ o) . g )

take h = (G ^ o) . g; :: thesis: ( g in A & h in B & h = (G ^ o) . g )

thus g in A by A3, A26, Lm8; :: thesis: ( h in B & h = (G ^ o) . g )

thus h in B by A3, Lm8; :: thesis: h = (G ^ o) . g

thus h = (G ^ o) . g by A27; :: thesis: verum

consider A, B being Element of Cosets N such that

A29: [y1,y2] = [A,B] and

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A28;

A in Cosets N by A3;

hence y1 in Cosets N by A29, XTUPLE_0:1; :: thesis: verum

now :: thesis: for y2 being object st y2 in rng f holds

y2 in Cosets N

then
rng f c= Cosets N
;y2 in Cosets N

let y2 be object ; :: thesis: ( y2 in rng f implies y2 in Cosets N )

assume y2 in rng f ; :: thesis: y2 in Cosets N

then consider y1 being object such that

A31: [y1,y2] in f by XTUPLE_0:def 13;

consider A, B being Element of Cosets N such that

A32: [y1,y2] = [A,B] and

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A31;

B in Cosets N by A3;

hence y2 in Cosets N by A32, XTUPLE_0:1; :: thesis: verum

end;assume y2 in rng f ; :: thesis: y2 in Cosets N

then consider y1 being object such that

A31: [y1,y2] in f by XTUPLE_0:def 13;

consider A, B being Element of Cosets N such that

A32: [y1,y2] = [A,B] and

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A31;

B in Cosets N by A3;

hence y2 in Cosets N by A32, XTUPLE_0:1; :: thesis: verum

hence H

for x being object st x in O holds

f . x = H

then consider IT being Function of O,(Funcs ((Cosets N),(Cosets N))) such that

A33: for x being object st x in O holds

IT . x = H

reconsider IT = IT as Action of O,(Cosets N) ;

take IT = IT; :: thesis: for o being Element of O holds IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

let o be Element of O; :: thesis: IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

reconsider x = o as set ;

set X = { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ;

set Y = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ;

A34: now :: thesis: for y being object holds

( ( y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) & ( y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) )

IT . o = { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds ( ( y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) & ( y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) )

let y be object ; :: thesis: ( ( y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) & ( y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) )

( g in A & h in B & h = (G ^ o) . g ) } ; :: thesis: y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

then consider A, B being Element of Cosets N such that

A37: y = [A,B] and

A38: ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) ;

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A38;

hence y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A37; :: thesis: verum

end;ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) & ( y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ) )

hereby :: thesis: ( y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } )

assume
y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st ( g in A & h in B & h = (G ^ o) . g ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } )

assume
y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ; :: thesis: y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

then consider A, B being Element of Cosets N such that

A35: y = [A,B] and

A36: for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) ;

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A36;

hence y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A35; :: thesis: verum

end;ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } ; :: thesis: y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

then consider A, B being Element of Cosets N such that

A35: y = [A,B] and

A36: for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) ;

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A36;

hence y in { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A35; :: thesis: verum

( g in A & h in B & h = (G ^ o) . g ) } ; :: thesis: y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) }

then consider A, B being Element of Cosets N such that

A37: y = [A,B] and

A38: ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) ;

for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) by A38;

hence y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A37; :: thesis: verum

ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A2, A33;

hence IT . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st

( g in A & h in B & h = (G ^ o) . g ) } by A34, TARSKI:2; :: thesis: verum

now :: thesis: ( O is empty implies ex IT being Action of O,(Cosets N) st IT = [:{},{(id (Cosets N))}:] )

hence
( ( not O is empty implies ex bassume
O is empty
; :: thesis: ex IT being Action of O,(Cosets N) st IT = [:{},{(id (Cosets N))}:]

then reconsider IT = [:{},{(id (Cosets N))}:] as Action of O,(Cosets N) by Lm1;

take IT = IT; :: thesis: IT = [:{},{(id (Cosets N))}:]

thus IT = [:{},{(id (Cosets N))}:] ; :: thesis: verum

end;then reconsider IT = [:{},{(id (Cosets N))}:] as Action of O,(Cosets N) by Lm1;

take IT = IT; :: thesis: IT = [:{},{(id (Cosets N))}:]

thus IT = [:{},{(id (Cosets N))}:] ; :: thesis: verum

for o being Element of O holds b

( g in A & h in B & h = (G ^ o) . g ) } ) & ( O is empty implies ex b