deffunc H1( set , set , set ) -> set = [:(H . $2,$3),(G . $1,$2):];
ex M being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
M . i,j,k = H1(i,j,k)
from ALTCAT_1:sch 3();
hence
ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . i,j,k = [:(H . j,k),(G . i,j):]
; verum