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 I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
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 I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
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 I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
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 I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
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 I1; :: thesis: for B being ManySortedSet of I2
for C being ManySortedSet of I3
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 I2; :: thesis: for C being ManySortedSet of I3
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 I3; :: 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 Def4;
reconsider F = F as ManySortedFunction of A,B * f by Def4;
A2: dom G = I1 by PARTFUN1:def 2;
A3: dom F = I1 by PARTFUN1:def 2;
A4: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def 19
.= I1 by A2, A3 ;
reconsider GF = G ** F as ManySortedSet of I1 ;
GF is ManySortedFunction of A,C * (g * f)

proof

let ii be object ; :: according to PBOOLE:def 15 :: thesis: ( not ii in I1 or GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] )
assume A5: 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 15;
reconsider Gi = G . ii as Function of ((B * f) . ii),((C * (g * f)) . ii) by A5, PBOOLE:def 15;
( not (B * f) . ii = {} or A . ii = {} or (C * (g * f)) . ii = {} ) by A1, A5;
then Gi * Fi is Function of (A . ii),((C * (g * f)) . ii) by FUNCT_2:13;
hence GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] by A4, A5, PBOOLE:def 19; :: thesis: verum

end;

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