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
A2: dom F = J by PARTFUN1:def 4;
set G = (Frege F) . f;
A3: dom ((Frege F) . f) = dom F by A1, Th8;
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;
A6: ((Frege F) . f) . x = (F . x) . (f . x) by A1, A3, A4, Th9;
f . x in dom (F . x) by A1, A3, A4, Th9;
then A7: y in rng (F . x) by A5, A6, FUNCT_1:def 5;
F . x is Function of (K . x),D by A2, A3, A4, Th6;
then rng (F . x) c= D by RELAT_1:def 19;
hence y in D by A7; :: thesis: verum

end;

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