let I be set ; :: thesis: for A, B, C being ManySortedSet of 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 ; :: 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 by MSSUBFAM:15;
GF is ManySortedFunction of A,C
proof
let i be
set ;
:: according to PBOOLE:def 18 :: 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 A3:
(
B . i = {} implies
A . i = {} )
by A1, PZFMISC1:def 3;
reconsider Gi =
G . i as
Function of
(B . i),
(C . i) by A2, PBOOLE:def 18;
reconsider Fi =
F . i as
Function of
(A . i),
(B . i) by A2, PBOOLE:def 18;
i in dom GF
by A2, PARTFUN1:def 4;
then
(G ** F) . i = Gi * Fi
by PBOOLE:def 24;
hence
GF . i is
Element of
bool [:(A . i),(C . i):]
by A3, FUNCT_2:19;
:: thesis: verum
end;
hence
G ** F is ManySortedFunction of A,C
; :: thesis: verum