now :: thesis: ( not O is empty implies for IT1, IT2 being Action of O,() 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,() 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,(); :: 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 b1, b2 being Action of O,() holds
( ( not O is empty & ( for o being Element of O holds b1 . 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 b2 . 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 b1 = b2 ) & ( O is empty & b1 = [:{},{(id ())}:] & b2 = [:{},{(id ())}:] implies b1 = b2 ) ) ; :: thesis: verum