set f = CayleyIso G;
let g1, g2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not g1 in dom (CayleyIso G) or not g2 in dom (CayleyIso G) or not (CayleyIso G) . g1 = (CayleyIso G) . g2 or g1 = g2 )
assume that
A1: ( g1 in dom (CayleyIso G) & g2 in dom (CayleyIso G) ) and
A2: (CayleyIso G) . g1 = (CayleyIso G) . g2 and
A3: g1 <> g2 ; :: thesis: contradiction
reconsider g1 = g1, g2 = g2 as Element of G by A1;
A4: ( (CayleyIso G) . g1 = * g1 & (CayleyIso G) . g2 = * g2 ) by Def4;
A5: dom (* g1) = the carrier of G by FUNCT_2:def 1;
A6: g1 " <> g2 " by A3, GROUP_1:9;
A7: (* g1) . (g1 ") = (g1 ") * g1 by TOPGRP_1:def 2
.= 1_ G by GROUP_1:def 5 ;
(* g2) . (g2 ") = (g2 ") * g2 by TOPGRP_1:def 2
.= 1_ G by GROUP_1:def 5 ;
hence contradiction by A2, A4, A5, A6, A7, FUNCT_1:def 4; :: thesis: verum