let G, H be trivial Group; :: thesis: G,H are_isomorphic
set h = 1: (G,H);
consider x being object such that
A1: the carrier of G = {x} by ZFMISC_1:131;
reconsider x = x as Element of G by A1, TARSKI:def 1;
consider y being object such that
A2: the carrier of H = {y} by ZFMISC_1:131;
reconsider y = y as Element of H by A2, TARSKI:def 1;
A4: 1_ H = y by A2, TARSKI:def 1;

now :: thesis: for z being object holds
( ( z in the carrier of H implies ex x being object st
( x in dom (1: (G,H)) & z = (1: (G,H)) . x ) ) & ( ex a being object st
( a in dom (1: (G,H)) & z = (1: (G,H)) . a ) implies z in the carrier of H ) )

let z be object ; :: thesis: ( ( z in the carrier of H implies ex x being object st
( x in dom (1: (G,H)) & z = (1: (G,H)) . x ) ) & ( ex a being object st
( a in dom (1: (G,H)) & z = (1: (G,H)) . a ) implies z in the carrier of H ) )

hereby :: thesis: ( ex a being object st
( a in dom (1: (G,H)) & z = (1: (G,H)) . a ) implies z in the carrier of H )

assume z in the carrier of H ; :: thesis: ex x being object st
( x in dom (1: (G,H)) & z = (1: (G,H)) . x )
then A5: z = y by A2, TARSKI:def 1;
reconsider x = x as object ;
take x = x; :: thesis: ( x in dom (1: (G,H)) & z = (1: (G,H)) . x )
thus x in dom (1: (G,H)) ; :: thesis: z = (1: (G,H)) . x
thus z = ( the carrier of G --> (1_ H)) . (1_ G) by A4, A5
.= (1: (G,H)) . x ; :: thesis: verum

end;

given a being object such that A6: ( a in dom (1: (G,H)) & z = (1: (G,H)) . a ) ; :: thesis: z in the carrier of H
A7: z in rng (1: (G,H)) by A6, FUNCT_1:3;
{(1_ H)} = rng ( the carrier of G --> (1_ H)) by FUNCOP_1:8
.= rng (1: (G,H)) ;
then z = 1_ H by A7, TARSKI:def 1;
hence z in the carrier of H ; :: thesis: verum

end;

then A8: rng (1: (G,H)) = the carrier of H by FUNCT_1:def 3;

now :: thesis: for a, b being object st a in dom (1: (G,H)) & b in dom (1: (G,H)) & (1: (G,H)) . a = (1: (G,H)) . b holds
a = b

let a, b be object ; :: thesis: ( a in dom (1: (G,H)) & b in dom (1: (G,H)) & (1: (G,H)) . a = (1: (G,H)) . b implies a = b )
assume ( a in dom (1: (G,H)) & b in dom (1: (G,H)) & (1: (G,H)) . a = (1: (G,H)) . b ) ; :: thesis: a = b
then ( a in dom (G --> (1_ H)) & b in dom (G --> (1_ H)) ) ;
then ( a = x & b = x ) by A1, TARSKI:def 1;
hence a = b ; :: thesis: verum

end;

then 1: (G,H) is one-to-one by FUNCT_1:def 4;
then 1: (G,H) is bijective by A8, FUNCT_2:def 3;
hence G,H are_isomorphic ; :: thesis: verum