let I be set ; 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; ( 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
; 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; for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C
let G be ManySortedFunction of B,C; 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 ;
PBOOLE:def 15 ( not i in I or GF . i is Element of bool [:(A . i),(C . i):] )
assume A2:
i in I
;
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;
verum
end;
hence
G ** F is ManySortedFunction of A,C
; verum