now :: thesis: ( not O is empty implies for IT1, IT2 being Action of O,(Cosets N) st ( 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 ) } ) & ( 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 ) } ) holds
IT1 = IT2 )

assume not O is empty ; :: thesis: for IT1, IT2 being Action of O,(Cosets N) st ( 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 ) } ) & ( 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 ) } ) holds
IT1 = IT2
let IT1, IT2 be Action of O,(Cosets N); :: thesis: ( ( 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 ) } ) & ( 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 ) } ) implies IT1 = IT2 )
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: ( ( 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 ) } ) implies IT1 = IT2 )
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: IT1 = IT2

A41: now :: thesis: for x being object st x in dom IT1 holds
IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
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: verum

end;

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

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