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