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:13;
hence F . j is Function of K . j,D by A1, PBOOLE:def 18; :: thesis: verum