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

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