consider M being ManySortedSet of [:F₁(),F₂():] such that
A1: for i, j being set st i in F₁() & j in F₂() holds
M . (i,j) = F₃(i,j) from ALTCAT_1:sch 1();
take M ; :: thesis: for i being Element of F₁()
for j being Element of F₂() holds M . (i,j) = F₃(i,j)
thus for i being Element of F₁()
for j being Element of F₂() holds M . (i,j) = F₃(i,j) by A1; :: thesis: verum