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)

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

hence
(J --> f) ** F is DoubleIndexedSet of K,B
by PBOOLE:def 15; :: thesis: verum
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;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