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 set such that
A3: the carrier of G = {e} by A2, GROUP_6:def 2;
consider g being Homomorphism of G,H such that
A4: g is bijective by A1, Def22;
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, Def25
.= {(g . e)} by A5, FUNCT_1:117 ;
hence H is trivial by GROUP_6:def 2; :: thesis: verum