A1: {|G|} . [i,j,k] = {|G|} . (i,j,k) by MULTOP_1:def 1
.= G . (i,k) by Def3 ;
A2: o . [i,j,k] = o . (i,j,k) by MULTOP_1:def 1;
{|G,G|} . [i,j,k] = {|G,G|} . (i,j,k) by MULTOP_1:def 1
.= [:(G . (j,k)),(G . (i,j)):] by Def4 ;
hence o . (i,j,k) is Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k)) by A2, A1, PBOOLE:def 15; :: thesis: verum