let G, H be strict Group; :: thesis: ( G is trivial & H is trivial implies G,H are_isomorphic )
assume ( G is trivial & H is trivial ) ; :: thesis: G,H are_isomorphic
then A1: ( G = (1). G & H = (1). H ) by Th13;
take 1: G,H ; :: according to GROUP_6:def 15 :: thesis: 1: G,H is bijective
set h = 1: G,H;
A2: 1: G,H is onto

proof

the carrier of ((1). G) = {(1_ G)} by GROUP_2:def 7;
then rng (1: G,H) = {((1: G,H) . (1_ G))} by A1, FUNCT_2:62
.= {(1_ H)} by Def8
.= the carrier of ((1). H) by GROUP_2:def 7 ;
hence 1: G,H is onto by A1, FUNCT_2:def 3; :: thesis: verum

end;

1: G,H is one-to-one

proof

now

let a, b be Element of G; :: thesis: ( (1: G,H) . a = (1: G,H) . b implies a = b )
assume (1: G,H) . a = (1: G,H) . b ; :: thesis: a = b
( a in the carrier of ((1). G) & b in the carrier of ((1). G) ) by A1;
then ( a in {(1_ G)} & b in {(1_ G)} ) by GROUP_2:def 7;
then ( a = 1_ G & b = 1_ G ) by TARSKI:def 1;
hence a = b ; :: thesis: verum

end;

then 1: G,H is one-to-one by Th1;
hence 1: G,H is one-to-one ; :: thesis: verum

end;

hence 1: G,H is bijective by A2; :: thesis: verum