let J, A be non empty set ; :: thesis: for B being set
for K being ManySortedSet of
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
let B be set ; :: thesis: for K being ManySortedSet of
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
let K be ManySortedSet of ; :: thesis: for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
let F be DoubleIndexedSet of K,A; :: thesis: for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
let f be Function of A,B; :: thesis: (J => f) ** F is DoubleIndexedSet of K,B
set fF = (J => f) ** F;
dom ((J => f) ** F) = J by MSUALG_3:2;
then reconsider fF = (J => f) ** F as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
for j being set st j in J holds
fF . j is Function of (K . j),((J --> B) . j)

proof

let j be set ; :: thesis: ( j in J implies fF . j is Function of (K . j),((J --> B) . j) )
assume A1: j in J ; :: thesis: fF . j is Function of (K . j),((J --> B) . j)
then reconsider j' = j as Element of J ;
reconsider Fj = F . j' as Function of (K . j),A ;
A2: (J --> B) . j = B by A1, FUNCOP_1:13;
fF . j = ((J => f) . j) * (F . j) by A1, MSUALG_3:2
.= f * Fj by FUNCOP_1:13 ;
hence fF . j is Function of (K . j),((J --> B) . j) by A2; :: thesis: verum

end;

hence (J --> f) ** F is DoubleIndexedSet of K,B by PBOOLE:def 18; :: thesis: verum