deffunc H₁( 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:
A3: Cosets N = Cosets H by Def14;

let x be object ; :: thesis:
set f = H₁(x);

A5: now :: thesis:

let y be object ; :: thesis:
assume y in H₁(x) ; :: thesis:
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:
take B = B; :: thesis:
thus y = [A,B] by A6; :: thesis:

end;

assume A7: x in O ; :: thesis:

now :: thesis:

reconsider o = x as Element of O by A7;
let y, y1, y2 be object ; :: thesis:
assume [y,y1] in H₁(x) ; :: thesis:
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₁(x) ; :: thesis:
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:

end;

then reconsider f = H₁(x) as Function by A5, FUNCT_1:def 1, RELAT_1:def 1;

now :: thesis:

let y1 be object ; :: thesis:

hereby :: thesis:

reconsider o = x as Element of O by A7;
assume A25: y1 in Cosets N ; :: thesis:
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:

now :: thesis:

let o be Element of O; :: thesis:
assume A27: x = o ; :: thesis:
take g = g; :: thesis:
take h = (G ^ o) . g; :: thesis:
thus g in A by A3, A26, Lm8; :: thesis:
thus h in B by A3, Lm8; :: thesis:
thus h = (G ^ o) . g by A27; :: thesis:

end;

hence [y1,y2] in f ; :: thesis:

end;

given y2 being object such that A28: [y1,y2] in f ; :: thesis:
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:

end;

then A30: dom f = Cosets N by XTUPLE_0:def 12;

now :: thesis:

let y2 be object ; :: thesis:
assume y2 in rng f ; :: thesis:
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:

end;

then rng f c= Cosets N ;
hence H₁(x) in Funcs ((Cosets N),(Cosets N)) by A30, FUNCT_2:def 2; :: thesis:

end;

ex f being Function of O,(Funcs ((Cosets N),(Cosets N))) st
for x being object st x in O holds
f . x = H₁(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₁(x) ;
reconsider IT = IT as Action of O,(Cosets N) ;
take IT = IT; :: thesis:
let o be Element of O; :: thesis:
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:

let y be object ; :: thesis:

hereby :: thesis:

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:
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:

end;

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 ) } ; :: thesis:
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:

end;

IT . o = { [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 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:

end;

now :: thesis:

assume O is empty ; :: thesis:
then reconsider IT = [:{},{(id (Cosets N))}:] as Action of O,(Cosets N) by Lm1;
take IT = IT; :: thesis:
thus IT = [:{},{(id (Cosets N))}:] ; :: thesis:

end;

hence ( ( not O is empty implies ex b₁ being Action of O,(Cosets N) st
for o being Element of O holds b₁ . 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 ) } ) & ( O is empty implies ex b₁ being Action of O,(Cosets N) st b₁ = [:{},{(id (Cosets N))}:] ) ) by A1; :: thesis: