let J, A be non empty set ; :: thesis: for B being set
for K being ManySortedSet of J
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 J
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 J; :: 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 J by PARTFUN1:def 2, RELAT_1:def 18;
for j being object st j in J holds
fF . j is Function of (K . j),((J --> B) . j)

proof

let j be object ; :: 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 j9 = j as Element of J ;
reconsider Fj = F . j9 as Function of (K . j),A ;
A2: fF . j = ((J => f) . j) * (F . j) by A1, MSUALG_3:2
.= f * Fj ;
thus 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 15; :: thesis: verum