let I1 be set ; 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 ; 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; 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; 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; 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; 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; 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; 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; ( ( 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 = {}
; 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 ;
PBOOLE:def 15 ( not ii in I1 or GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] )
assume A5:
ii in I1
;
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;
verum
end;
hence
G ** F is MSUnTrans of g * f,A,C
by Def4; verum