let J, D be set ; :: thesis: for K being ManySortedSet of J

for F being DoubleIndexedSet of K,D

for j being set st j in J holds

F . j is Function of (K . j),D

let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,D

for j being set st j in J holds

F . j is Function of (K . j),D

let F be DoubleIndexedSet of K,D; :: thesis: for j being set st j in J holds

F . j is Function of (K . j),D

let j be set ; :: thesis: ( j in J implies F . j is Function of (K . j),D )

assume A1: j in J ; :: thesis: F . j is Function of (K . j),D

then (J --> D) . j = D by FUNCOP_1:7;

hence F . j is Function of (K . j),D by A1, PBOOLE:def 15; :: thesis: verum

for F being DoubleIndexedSet of K,D

for j being set st j in J holds

F . j is Function of (K . j),D

let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,D

for j being set st j in J holds

F . j is Function of (K . j),D

let F be DoubleIndexedSet of K,D; :: thesis: for j being set st j in J holds

F . j is Function of (K . j),D

let j be set ; :: thesis: ( j in J implies F . j is Function of (K . j),D )

assume A1: j in J ; :: thesis: F . j is Function of (K . j),D

then (J --> D) . j = D by FUNCOP_1:7;

hence F . j is Function of (K . j),D by A1, PBOOLE:def 15; :: thesis: verum