consider M being ManySortedSet of [:F_{1}(),F_{2}(),F_{3}():] such that

A1: for i, j, k being set st i in F_{1}() & j in F_{2}() & k in F_{3}() holds

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

take M ; :: thesis: for i being Element of F_{1}()

for j being Element of F_{2}()

for k being Element of F_{3}() holds M . (i,j,k) = F_{4}(i,j,k)

thus for i being Element of F_{1}()

for j being Element of F_{2}()

for k being Element of F_{3}() holds M . (i,j,k) = F_{4}(i,j,k)
by A1; :: thesis: verum

A1: for i, j, k being set st i in F

M . (i,j,k) = F

take M ; :: thesis: for i being Element of F

for j being Element of F

for k being Element of F

thus for i being Element of F

for j being Element of F

for k being Element of F