let J, D be set ; :: thesis: for K being ManySortedSet of
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 ; :: 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:13;
hence F . j is Function of (K . j),D by A1, PBOOLE:def 18; :: thesis: verum