deffunc H1( object , object , object ) -> set = [:(H . ($2,$3)),(G . ($1,$2)):];
consider M being ManySortedSet of [:I,I,I:] such that
A5:
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();
take
M
; for i, j, k being object st i in I & j in I & k in I holds
M . (i,j,k) = [:(H . (j,k)),(G . (i,j)):]
let i, j, k be object ; ( i in I & j in I & k in I implies M . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] )
thus
( i in I & j in I & k in I implies M . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] )
by A5; verum