let J, D be set ; :: thesis: for K being ManySortedSet of
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D
let K be ManySortedSet of ; :: thesis: for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D
let F be DoubleIndexedSet of K,D; :: thesis: for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D
let f be Function; :: thesis: ( f in dom (Frege F) implies (Frege F) . f is Function of J,D )
assume A1: f in dom (Frege F) ; :: thesis: (Frege F) . f is Function of J,D
set G = (Frege F) . f;
A2: dom ((Frege F) . f) = dom F by A1, Th8;
A3: dom F = J by PARTFUN1:def 4;
rng ((Frege F) . f) c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Frege F) . f) or y in D )
assume y in rng ((Frege F) . f) ; :: thesis: y in D
then consider x being set such that
A4: x in dom ((Frege F) . f) and
A5: y = ((Frege F) . f) . x by FUNCT_1:def 5;
F . x is Function of (K . x),D by A3, 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 A5, FUNCT_1:def 5;
hence y in D by A6; :: thesis: verum

end;

hence (Frege F) . f is Function of J,D by A3, A2, FUNCT_2:4; :: thesis: verum