consider M being ManySortedSet of [:F1(),F2():] such that
A1: for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j) from ALTCAT_1:sch 2();
 A2: dom M = [:F1(),F2():] by PARTFUN1:def 2;
rng M c= F3()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng M or y in F3() )
assume y in rng M ; :: thesis: y in F3()
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 F1() & x2 in F2() & x = [x1,x2] ) by A3, ZFMISC_1:def 2;
y = M . (x1,x2) by A3, A4
.= F4(x1,x2) by A1, A4 ;
hence y in F3() ; :: thesis: verum
end;
then reconsider M = M as Function of [:F1(),F2():],F3() by A2, FUNCT_2:2;
take M ; :: thesis: for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j)
thus for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j) by A1; :: thesis: verum