A1: {|G|} . [i,j,k] = {|G|} . i,j,k by MULTOP_1:def 1
.= G . i,k by Def5 ;
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 Def6 ;
hence o . i,j,k is Function of [:(G . j,k),(G . i,j):],(G . i,k) by A2, A1, PBOOLE:def 18; :: thesis: verum