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

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

hence
G ** F is ManySortedFunction of A,C
; :: thesis: verum
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;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