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

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