now :: thesis:

assume not O is empty ; :: thesis:
let IT1, IT2 be Action of O,(Cosets N); :: thesis:
assume A39: for o being Element of O holds IT1 . 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 ) } ; :: thesis:
assume A40: for o being Element of O holds IT2 . 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 ) } ; :: thesis:

A41: now :: thesis:

let x be object ; :: thesis:
assume x in dom IT1 ; :: thesis:
then reconsider o = x as Element of O ;
IT1 . 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 A39;
hence IT1 . x = IT2 . x by A40; :: thesis:

end;

( dom IT1 = O & dom IT2 = O ) by FUNCT_2:def 1;
hence IT1 = IT2 by A41; :: thesis:

end;

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