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

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