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

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) by A4;
then a in {(1_ G)} by GROUP_2:def 7;
then A5: a = 1_ G by TARSKI:def 1;
b in the carrier of ((1). G) by A4;
then b in {(1_ G)} by GROUP_2:def 7;
hence a = b by A5, TARSKI:def 1; :: thesis: verum

end;

then A6: 1: G,H is one-to-one by Th1;
the carrier of ((1). G) = {(1_ G)} by GROUP_2:def 7;
then rng (1: G,H) = {((1: G,H) . (1_ G))} by A4, FUNCT_2:62
.= {(1_ H)} by Def8
.= the carrier of ((1). H) by GROUP_2:def 7 ;
then 1: G,H is onto by A3, FUNCT_2:def 3;
hence 1: G,H is bijective by A6; :: thesis: verum