consider M being ManySortedSet of [:F₁(),F₂():] such that
A1: for i being Element of F₁()
for j being Element of F₂() holds M . (i,j) = F₄(i,j) from ALTCAT_1:sch 2();
A2: dom M = [:F₁(),F₂():] by PARTFUN1:def 2;
rng M c= F₃()

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng M or y in F₃() )
assume y in rng M ; :: thesis: y in F₃()
then consider x being object such that
A3: ( x in dom M & y = M . x ) by FUNCT_1:def 3;
consider x1, x2 being object such that
A4: ( x1 in F₁() & x2 in F₂() & x = [x1,x2] ) by A3, ZFMISC_1:def 2;
y = M . (x1,x2) by A3, A4
.= F₄(x1,x2) by A1, A4 ;
hence y in F₃() ; :: thesis: verum

end;

then reconsider M = M as Function of [:F₁(),F₂():],F₃() by A2, FUNCT_2:2;
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