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 11 :: thesis: 1: (G,H) is bijective
A3: H = (1). H by A2, Th12;
set h = 1: (G,H);
A4: G = (1). G by A1, Th12;
now :: thesis: for a, b being Element of G st (1: (G,H)) . a = (1: (G,H)) . b holds
a = b
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:48
.= {(1_ H)} by FUNCOP_1:7
.= the carrier of ((1). H) by GROUP_2:def 7 ;
then 1: (G,H) is onto by A3;
hence 1: (G,H) is bijective by A6; :: thesis: verum