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 (Frege F) holds

(Frege F) . 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 (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 2;

rng ((Frege F) . f) c= D

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 J; :: 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 2;

rng ((Frege F) . f) c= D

proof

hence
(Frege F) . f is Function of J,D
by A3, A2, FUNCT_2:2; :: thesis: verum
let y be object ; :: 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 object such that

A4: x in dom ((Frege F) . f) and

A5: y = ((Frege F) . 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 A5, FUNCT_1:def 3;

hence y in D by A6; :: thesis: verum

end;assume y in rng ((Frege F) . f) ; :: thesis: y in D

then consider x being object such that

A4: x in dom ((Frege F) . f) and

A5: y = ((Frege F) . 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 A5, FUNCT_1:def 3;

hence y in D by A6; :: thesis: verum