let J, D be set ; :: thesis: for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for f being Function st f in dom () holds
() . f is Function of J,D

let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,D
for f being Function st f in dom () holds
() . f is Function of J,D

let F be DoubleIndexedSet of K,D; :: thesis: for f being Function st f in dom () holds
() . f is Function of J,D

let f be Function; :: thesis: ( f in dom () implies () . f is Function of J,D )
assume A1: f in dom () ; :: thesis: () . f is Function of J,D
set G = () . f;
A2: dom (() . f) = dom F by ;
A3: dom F = J by PARTFUN1:def 2;
rng (() . f) c= D
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (() . f) or y in D )
assume y in rng (() . f) ; :: thesis: y in D
then consider x being object such that
A4: x in dom (() . f) and
A5: y = (() . f) . x by FUNCT_1:def 3;
F . x is Function of (K . x),D by A2, A4, Th6;
then A6: rng (F . x) c= D by RELAT_1:def 19;
( ((Frege F) . f) . x = (F . x) . (f . x) & f . x in dom (F . x) ) by A1, A2, A4, Th9;
then y in rng (F . x) by ;
hence y in D by A6; :: thesis: verum
end;
hence (Frege F) . f is Function of J,D by ; :: thesis: verum