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

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

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

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

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

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

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

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

M . (i,j) = F

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

for j being Element of F

thus for i being Element of F

for j being Element of F