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 )

hence
for b( 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

hence IT1 = IT2 by A41; :: thesis: verum

end;( 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

( dom IT1 = O & dom IT2 = O )
by FUNCT_2:def 1;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;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

hence IT1 = IT2 by A41; :: thesis: verum

( ( not O is empty & ( for o being Element of O holds b

( g in A & h in B & h = (G ^ o) . g ) } ) & ( for o being Element of O holds b

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