let I1 be set ; :: thesis: for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of
for B being ManySortedSet of
for C being ManySortedSet of
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let I2, I3 be non empty set ; :: thesis: for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of
for B being ManySortedSet of
for C being ManySortedSet of
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let f be Function of I1,I2; :: thesis: for g being Function of I2,I3
for A being ManySortedSet of
for B being ManySortedSet of
for C being ManySortedSet of
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let g be Function of I2,I3; :: thesis: for A being ManySortedSet of
for B being ManySortedSet of
for C being ManySortedSet of
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let A be ManySortedSet of ; :: thesis: for B being ManySortedSet of
for C being ManySortedSet of
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let B be ManySortedSet of ; :: thesis: for C being ManySortedSet of
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let C be ManySortedSet of ; :: thesis: for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let F be MSUnTrans of f,A,B; :: thesis: for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let G be MSUnTrans of g * f,B * f,C; :: thesis: ( ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) implies G ** F is MSUnTrans of g * f,A,C )
assume A1: for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ; :: thesis: G ** F is MSUnTrans of g * f,A,C
reconsider G = G as ManySortedFunction of B * f,C * (g * f) by Def5;
reconsider F = F as ManySortedFunction of A,B * f by Def5;
A2: ( dom G = I1 & dom F = I1 ) by PARTFUN1:def 4;
A3: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def 24
.= I1 by A2 ;
reconsider GF = G ** F as ManySortedSet of ;
GF is ManySortedFunction of A,C * (g * f)

proof

let ii be set ; :: according to PBOOLE:def 18 :: thesis: ( not ii in I1 or GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] )
assume A4: ii in I1 ; :: thesis: GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):]
then reconsider Fi = F . ii as Function of (A . ii),((B * f) . ii) by PBOOLE:def 18;
reconsider Gi = G . ii as Function of ((B * f) . ii),((C * (g * f)) . ii) by A4, PBOOLE:def 18;
( not (B * f) . ii = {} or A . ii = {} or (C * (g * f)) . ii = {} ) by A1, A4;
then Gi * Fi is Function of (A . ii),((C * (g * f)) . ii) by FUNCT_2:19;
hence GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] by A3, A4, PBOOLE:def 24; :: thesis: verum

end;

hence G ** F is MSUnTrans of g * f,A,C by Def5; :: thesis: verum