let i, I be set ; for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
let M be ManySortedSet of I; for f being Function
for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
let f be Function; for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
let P be MSSetOp of M; ( P is topological & i in I & f = P . i implies for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y) )
assume that
A1:
P is topological
and
A2:
i in I
and
A3:
f = P . i
; for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)
A4:
i in dom P
by A2, PARTFUN1:def 2;
let x, y be Element of bool (M . i); f . (x \/ y) = (f . x) \/ (f . y)
dom ((EmptyMS I) +* (i .--> y)) = I
by A2, PZFMISC1:1;
then reconsider Y = (EmptyMS I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
dom ((EmptyMS I) +* (i .--> x)) = I
by A2, PZFMISC1:1;
then reconsider X = (EmptyMS I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A5:
i in {i}
by TARSKI:def 1;
dom (i .--> y) = {i}
;
then A6: Y . i =
(i .--> y) . i
by A5, FUNCT_4:13
.=
y
by FUNCOP_1:72
;
A7:
( X is Element of bool M & Y is Element of bool M )
by Lm2, MSSUBFAM:11;
i in dom (X (\/) Y)
by A2, PARTFUN1:def 2;
then
i in (dom P) /\ (dom (X (\/) Y))
by A4, XBOOLE_0:def 4;
then B1:
i in dom (P .. (X (\/) Y))
by PRALG_1:def 19;
i in dom X
by A2, PARTFUN1:def 2;
then
i in (dom P) /\ (dom X)
by XBOOLE_0:def 4, A4;
then B2:
i in dom (P .. X)
by PRALG_1:def 19;
i in dom Y
by A2, PARTFUN1:def 2;
then
i in (dom P) /\ (dom Y)
by XBOOLE_0:def 4, A4;
then B3:
i in dom (P .. Y)
by PRALG_1:def 19;
dom (i .--> x) = {i}
;
then A8: X . i =
(i .--> x) . i
by A5, FUNCT_4:13
.=
x
by FUNCOP_1:72
;
hence f . (x \/ y) =
f . ((X (\/) Y) . i)
by A2, A6, PBOOLE:def 4
.=
(P .. (X (\/) Y)) . i
by A3, PRALG_1:def 19, B1
.=
((P .. X) (\/) (P .. Y)) . i
by A1, A7
.=
((P .. X) . i) \/ ((P .. Y) . i)
by A2, PBOOLE:def 4
.=
(f . (X . i)) \/ ((P .. Y) . i)
by A3, PRALG_1:def 19, B2
.=
(f . x) \/ (f . y)
by A3, A8, A6, PRALG_1:def 19, B3
;
verum