let i, I be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: 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 ;
:: thesis: verum