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