let I be set ; :: thesis: for A, B, C being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let A, B, C be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C )
assume A1: A is_transformable_to B ; :: thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let G be ManySortedFunction of B,C; :: thesis: G ** F is ManySortedFunction of A,C
reconsider GF = G ** F as ManySortedFunction of I by MSSUBFAM:15;
GF is ManySortedFunction of A,C

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or GF . i is Element of bool [:(A . i),(C . i):] )
assume A2: i in I ; :: thesis: GF . i is Element of bool [:(A . i),(C . i):]
then reconsider Gi = G . i as Function of (B . i),(C . i) by PBOOLE:def 15;
reconsider Fi = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def 15;
i in dom GF by A2, PARTFUN1:def 2;
then A3: (G ** F) . i = Gi * Fi by PBOOLE:def 19;
( B . i = {} implies A . i = {} ) by A1, A2, PZFMISC1:def 3;
hence GF . i is Element of bool [:(A . i),(C . i):] by A3, FUNCT_2:13; :: thesis: verum

end;

hence G ** F is ManySortedFunction of A,C ; :: thesis: verum