set c = the carrier of G;
set f = CayleyIso G;
let g1, g2 be Element of G; :: according to GROUP_6:def 6 :: thesis: (CayleyIso G) . (g1 * g2) = ((CayleyIso G) . g1) * ((CayleyIso G) . g2)
A1: (CayleyIso G) . (g1 * g2) is Permutation of the carrier of G by Th5;
then A2: dom ((CayleyIso G) . (g1 * g2)) = the carrier of G by FUNCT_2:def 1;
((CayleyIso G) . g1) * ((CayleyIso G) . g2) is Permutation of the carrier of G by Th5;
then A3: dom (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) = the carrier of G by FUNCT_2:def 1;

now :: thesis: for y being object st y in dom ((CayleyIso G) . (g1 * g2)) holds
((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y

let y be object ; :: thesis: ( y in dom ((CayleyIso G) . (g1 * g2)) implies ((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y )
assume y in dom ((CayleyIso G) . (g1 * g2)) ; :: thesis: ((CayleyIso G) . (g1 * g2)) . y = (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y
then reconsider x = y as Element of G by A1, FUNCT_2:def 1;
thus ((CayleyIso G) . (g1 * g2)) . y = (* (g1 * g2)) . x by Def4
.= x * (g1 * g2) by TOPGRP_1:def 2
.= (x * g1) * g2 by GROUP_1:def 3
.= (* g2) . (x * g1) by TOPGRP_1:def 2
.= (* g2) . ((* g1) . x) by TOPGRP_1:def 2
.= ((* g2) * (* g1)) . x by FUNCT_2:15
.= (((CayleyIso G) . g2) * (* g1)) . x by Def4
.= (((CayleyIso G) . g2) * ((CayleyIso G) . g1)) . y by Def4
.= (((CayleyIso G) . g1) * ((CayleyIso G) . g2)) . y by Def2 ; :: thesis: verum

end;

hence (CayleyIso G) . (g1 * g2) = ((CayleyIso G) . g1) * ((CayleyIso G) . g2) by A2, A3; :: thesis: verum