let J, D be set ; 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; 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; for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D
let f be Function; ( f in dom (Frege F) implies (Frege F) . f is Function of J,D )
assume A1:
f in dom (Frege F)
; (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
hence
(Frege F) . f is Function of J,D
by A3, A2, FUNCT_2:2; verum