deffunc H_{1}( object , object , object ) -> set = G . ($1,$3);

consider M being ManySortedSet of [:I,I,I:] such that

A1: for i, j, k being set st i in I & j in I & k in I holds

M . (i,j,k) = H_{1}(i,j,k)
from ALTCAT_1:sch 3();

take M ; :: thesis: for i, j, k being object st i in I & j in I & k in I holds

M . (i,j,k) = G . (i,k)

let i, j, k be object ; :: thesis: ( i in I & j in I & k in I implies M . (i,j,k) = G . (i,k) )

thus ( i in I & j in I & k in I implies M . (i,j,k) = G . (i,k) ) by A1; :: thesis: verum

consider M being ManySortedSet of [:I,I,I:] such that

A1: for i, j, k being set st i in I & j in I & k in I holds

M . (i,j,k) = H

take M ; :: thesis: for i, j, k being object st i in I & j in I & k in I holds

M . (i,j,k) = G . (i,k)

let i, j, k be object ; :: thesis: ( i in I & j in I & k in I implies M . (i,j,k) = G . (i,k) )

thus ( i in I & j in I & k in I implies M . (i,j,k) = G . (i,k) ) by A1; :: thesis: verum