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 4;
let x, y be Element of bool (M . i); f . (x \/ y) = (f . x) \/ (f . y)
dom (([[0]] I) +* (i .--> y)) = I
by A2, PZFMISC1:1;
then reconsider Y = ([[0]] I) +* (i .--> y) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
dom (([[0]] I) +* (i .--> x)) = I
by A2, PZFMISC1:1;
then reconsider X = ([[0]] I) +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A5:
i in {i}
by TARSKI:def 1;
dom (i .--> y) = {i}
by FUNCOP_1:19;
then A6: Y . i =
(i .--> y) . i
by A5, FUNCT_4:14
.=
y
by FUNCOP_1:87
;
A7:
( X is Element of bool M & Y is Element of bool M )
by Lm2, MSSUBFAM:11;
dom (i .--> x) = {i}
by FUNCOP_1:19;
then A8: X . i =
(i .--> x) . i
by A5, FUNCT_4:14
.=
x
by FUNCOP_1:87
;
hence f . (x \/ y) =
f . ((X \/ Y) . i)
by A2, A6, PBOOLE:def 7
.=
(P .. (X \/ Y)) . i
by A3, A4, PRALG_1:def 17
.=
((P .. X) \/ (P .. Y)) . i
by A1, A7, Def5
.=
((P .. X) . i) \/ ((P .. Y) . i)
by A2, PBOOLE:def 7
.=
(f . (X . i)) \/ ((P .. Y) . i)
by A3, A4, PRALG_1:def 17
.=
(f . x) \/ (f . y)
by A3, A8, A6, A4, PRALG_1:def 17
;
verum