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 ;
i in dom GF by ;
then A3: (G ** F) . i = Gi * Fi by PBOOLE:def 19;
( B . i = {} implies A . i = {} ) by ;
hence GF . i is Element of bool [:(A . i),(C . i):] by ; :: thesis: verum
end;
hence G ** F is ManySortedFunction of A,C ; :: thesis: verum