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 Def5;
reconsider F = F as ManySortedFunction of A,B * f by Def5;
A2: ( dom G = I1 & dom F = I1 ) by PBOOLE:def 3;
A3: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def 24
.= I1 by A2 ;
reconsider GF = G ** F as ManySortedSet of I1 ;
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 Relation of A . ii,(C * (g * f)) . ii )
assume A4: ii in I1 ; :: thesis: GF . ii is Relation of 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 Function of 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