deffunc H₁( set , set , set ) -> set = G . ($1,$3);
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) = H₁(i,j,k) from ALTCAT_1:sch 3();
hence ex b₁ being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b₁ . (i,j,k) = G . (i,k) ; :: thesis: verum