let O be set ; :: thesis: for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is trivial holds
H is trivial
let G, H be strict GroupWithOperators of O; :: thesis: ( G,H are_isomorphic & G is trivial implies H is trivial )
assume that
A1: G,H are_isomorphic and
A2: G is trivial ; :: thesis: H is trivial
consider e being object such that
A3: the carrier of G = {e} by A2;
consider g being Homomorphism of G,H such that
A4: g is bijective by A1;
e in the carrier of G by A3, TARSKI:def 1;
then A5: e in dom g by FUNCT_2:def 1;
the carrier of H = the carrier of (Image g) by A4, Th51
.= Im (g,e) by A3, Def22
.= {(g . e)} by A5, FUNCT_1:59 ;
hence H is trivial ; :: thesis: verum