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

.= 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