let J be set ; :: thesis: for K being ManySortedSet of J
for D being non empty set
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
f . j in K . j
let K be ManySortedSet of J; :: thesis: for D being non empty set
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
f . j in K . j
let D be non empty set ; :: thesis: for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
f . j in K . j
let F be DoubleIndexedSet of K,D; :: thesis: for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
f . j in K . j
let f be Function; :: thesis: ( f in dom (Frege F) implies for j being set st j in J holds
f . j in K . j )
assume A1: f in dom (Frege F) ; :: thesis: for j being set st j in J holds
f . j in K . j
let j be set ; :: thesis: ( j in J implies f . j in K . j )
assume A2: j in J ; :: thesis: f . j in K . j
A3: F . j is Function of (K . j),D by A2, Th6;
dom F = J by PARTFUN1:def 2;
then f . j in dom (F . j) by A1, A2, Th9;
hence f . j in K . j by A3, FUNCT_2:def 1; :: thesis: verum