let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL
for B being set st B c= dom (f + g) holds
( dom ((f + g) | B) = B & dom ((f | B) + (g | B)) = B & (f + g) | B = (f | B) + (g | B) )
let f, g be PartFunc of X,ExtREAL ; :: thesis: for B being set st B c= dom (f + g) holds
( dom ((f + g) | B) = B & dom ((f | B) + (g | B)) = B & (f + g) | B = (f | B) + (g | B) )
let B be set ; :: thesis: ( B c= dom (f + g) implies ( dom ((f + g) | B) = B & dom ((f | B) + (g | B)) = B & (f + g) | B = (f | B) + (g | B) ) )
assume A1: B c= dom (f + g) ; :: thesis: ( dom ((f + g) | B) = B & dom ((f | B) + (g | B)) = B & (f + g) | B = (f | B) + (g | B) )
dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
then dom (f + g) c= (dom f) /\ (dom g) by XBOOLE_1:36;
then A2: B c= (dom f) /\ (dom g) by A1, XBOOLE_1:1;
for x being set st x in dom (f | B) holds
(f | B) . x in ExtREAL ;
then reconsider fb = f | B as Function of (dom (f | B)),ExtREAL by FUNCT_2:5;
for x being set st x in dom f holds
f . x in ExtREAL ;
then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:5;
for x being set st x in dom (g | B) holds
(g | B) . x in ExtREAL ;
then reconsider gb = g | B as Function of (dom (g | B)),ExtREAL by FUNCT_2:5;
for x being set st x in dom g holds
g . x in ExtREAL ;
then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:5;
( dom ((f + g) | B) = (dom (f + g)) /\ B & dom (f | B) = (dom f) /\ B & dom (g | B) = (dom g) /\ B ) by RELAT_1:90;
then A3: ( dom ((f + g) | B) = B & dom (f | B) = B & dom (g | B) = B ) by A1, A2, XBOOLE_1:18, XBOOLE_1:28;
A4: (f | B) " {+infty } = (f " {+infty }) /\ B

proof

now

let x be set ; :: thesis: ( x in (f | B) " {+infty } implies x in (f " {+infty }) /\ B )
assume x in (f | B) " {+infty } ; :: thesis: x in (f " {+infty }) /\ B
then A5: ( x in dom fb & fb . x in {+infty } ) by FUNCT_2:46;
then ( x in (dom f) /\ B & (f | B) . x in {+infty } ) by RELAT_1:90;
then ( x in dom f & x in B & f . x in {+infty } ) by A5, FUNCT_1:70, XBOOLE_0:def 4;
then ( x in ff " {+infty } & x in B ) by FUNCT_2:46;
hence x in (f " {+infty }) /\ B by XBOOLE_0:def 4; :: thesis: verum

end;

then A6: (f | B) " {+infty } c= (f " {+infty }) /\ B by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (f " {+infty }) /\ B implies x in (f | B) " {+infty } )
assume x in (f " {+infty }) /\ B ; :: thesis: x in (f | B) " {+infty }
then ( x in f " {+infty } & x in B ) by XBOOLE_0:def 4;
then ( x in dom ff & ff . x in {+infty } & x in B ) by FUNCT_2:46;
then ( x in (dom ff) /\ B & ff . x in {+infty } ) by XBOOLE_0:def 4;
then ( x in dom (ff | B) & ff . x in {+infty } ) by RELAT_1:90;
then ( x in dom fb & fb . x in {+infty } ) by FUNCT_1:70;
hence x in (f | B) " {+infty } by FUNCT_2:46; :: thesis: verum

end;

then (f " {+infty }) /\ B c= (f | B) " {+infty } by TARSKI:def 3;
hence (f | B) " {+infty } = (f " {+infty }) /\ B by A6, XBOOLE_0:def 10; :: thesis: verum

end;

A7: (f | B) " {-infty } = (f " {-infty }) /\ B

proof

now

let x be set ; :: thesis: ( x in (f | B) " {-infty } implies x in (f " {-infty }) /\ B )
assume x in (f | B) " {-infty } ; :: thesis: x in (f " {-infty }) /\ B
then A8: ( x in dom fb & fb . x in {-infty } ) by FUNCT_2:46;
then ( x in (dom f) /\ B & (f | B) . x in {-infty } ) by RELAT_1:90;
then ( x in dom f & x in B & f . x in {-infty } ) by A8, FUNCT_1:70, XBOOLE_0:def 4;
then ( x in ff " {-infty } & x in B ) by FUNCT_2:46;
hence x in (f " {-infty }) /\ B by XBOOLE_0:def 4; :: thesis: verum

end;

then A9: (f | B) " {-infty } c= (f " {-infty }) /\ B by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (f " {-infty }) /\ B implies x in (f | B) " {-infty } )
assume x in (f " {-infty }) /\ B ; :: thesis: x in (f | B) " {-infty }
then ( x in f " {-infty } & x in B ) by XBOOLE_0:def 4;
then ( x in dom ff & ff . x in {-infty } & x in B ) by FUNCT_2:46;
then ( x in (dom ff) /\ B & ff . x in {-infty } ) by XBOOLE_0:def 4;
then ( x in dom (ff | B) & ff . x in {-infty } ) by RELAT_1:90;
then ( x in dom fb & fb . x in {-infty } ) by FUNCT_1:70;
hence x in (f | B) " {-infty } by FUNCT_2:46; :: thesis: verum

end;

then (f " {-infty }) /\ B c= (f | B) " {-infty } by TARSKI:def 3;
hence (f | B) " {-infty } = (f " {-infty }) /\ B by A9, XBOOLE_0:def 10; :: thesis: verum

end;

A10: (g | B) " {+infty } = (g " {+infty }) /\ B

proof

now

let x be set ; :: thesis: ( x in (g | B) " {+infty } implies x in (g " {+infty }) /\ B )
assume x in (g | B) " {+infty } ; :: thesis: x in (g " {+infty }) /\ B
then A11: ( x in dom gb & gb . x in {+infty } ) by FUNCT_2:46;
then ( x in (dom g) /\ B & (g | B) . x in {+infty } ) by RELAT_1:90;
then ( x in dom g & x in B & g . x in {+infty } ) by A11, FUNCT_1:70, XBOOLE_0:def 4;
then ( x in gg " {+infty } & x in B ) by FUNCT_2:46;
hence x in (g " {+infty }) /\ B by XBOOLE_0:def 4; :: thesis: verum

end;

then A12: (g | B) " {+infty } c= (g " {+infty }) /\ B by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (g " {+infty }) /\ B implies x in (g | B) " {+infty } )
assume x in (g " {+infty }) /\ B ; :: thesis: x in (g | B) " {+infty }
then ( x in g " {+infty } & x in B ) by XBOOLE_0:def 4;
then ( x in dom gg & gg . x in {+infty } & x in B ) by FUNCT_2:46;
then ( x in (dom gg) /\ B & gg . x in {+infty } ) by XBOOLE_0:def 4;
then ( x in dom (gg | B) & gg . x in {+infty } ) by RELAT_1:90;
then ( x in dom gb & gb . x in {+infty } ) by FUNCT_1:70;
hence x in (g | B) " {+infty } by FUNCT_2:46; :: thesis: verum

end;

then (g " {+infty }) /\ B c= (g | B) " {+infty } by TARSKI:def 3;
hence (g | B) " {+infty } = (g " {+infty }) /\ B by A12, XBOOLE_0:def 10; :: thesis: verum

end;

A13: (g | B) " {-infty } = (g " {-infty }) /\ B

proof

now

let x be set ; :: thesis: ( x in (g | B) " {-infty } implies x in (g " {-infty }) /\ B )
assume x in (g | B) " {-infty } ; :: thesis: x in (g " {-infty }) /\ B
then A14: ( x in dom gb & gb . x in {-infty } ) by FUNCT_2:46;
then ( x in (dom g) /\ B & (g | B) . x in {-infty } ) by RELAT_1:90;
then ( x in dom g & x in B & g . x in {-infty } ) by A14, FUNCT_1:70, XBOOLE_0:def 4;
then ( x in gg " {-infty } & x in B ) by FUNCT_2:46;
hence x in (g " {-infty }) /\ B by XBOOLE_0:def 4; :: thesis: verum

end;

then A15: (g | B) " {-infty } c= (g " {-infty }) /\ B by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (g " {-infty }) /\ B implies x in (g | B) " {-infty } )
assume x in (g " {-infty }) /\ B ; :: thesis: x in (g | B) " {-infty }
then ( x in g " {-infty } & x in B ) by XBOOLE_0:def 4;
then ( x in dom gg & gg . x in {-infty } & x in B ) by FUNCT_2:46;
then ( x in (dom gg) /\ B & gg . x in {-infty } ) by XBOOLE_0:def 4;
then ( x in dom (gg | B) & gg . x in {-infty } ) by RELAT_1:90;
then ( x in dom gb & gb . x in {-infty } ) by FUNCT_1:70;
hence x in (g | B) " {-infty } by FUNCT_2:46; :: thesis: verum

end;

then (g " {-infty }) /\ B c= (g | B) " {-infty } by TARSKI:def 3;
hence (g | B) " {-infty } = (g " {-infty }) /\ B by A15, XBOOLE_0:def 10; :: thesis: verum

end;

A16: ((f | B) " {-infty }) /\ ((g | B) " {+infty }) = (((f " {-infty }) /\ B) /\ (g " {+infty })) /\ B by A7, A10, XBOOLE_1:16
.= (((f " {-infty }) /\ (g " {+infty })) /\ B) /\ B by XBOOLE_1:16
.= ((f " {-infty }) /\ (g " {+infty })) /\ (B /\ B) by XBOOLE_1:16 ;
((f | B) " {+infty }) /\ ((g | B) " {-infty }) = (((f " {+infty }) /\ B) /\ (g " {-infty })) /\ B by A4, A13, XBOOLE_1:16
.= (((f " {+infty }) /\ (g " {-infty })) /\ B) /\ B by XBOOLE_1:16
.= ((f " {+infty }) /\ (g " {-infty })) /\ (B /\ B) by XBOOLE_1:16 ;
then A17: (((f | B) " {-infty }) /\ ((g | B) " {+infty })) \/ (((f | B) " {+infty }) /\ ((g | B) " {-infty })) = (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) /\ B by A16, XBOOLE_1:23;
(dom (f | B)) /\ (dom (g | B)) = ((dom f) /\ B) /\ (dom (g | B)) by RELAT_1:90
.= ((dom f) /\ B) /\ ((dom g) /\ B) by RELAT_1:90
.= (((dom f) /\ B) /\ (dom g)) /\ B by XBOOLE_1:16
.= (((dom f) /\ (dom g)) /\ B) /\ B by XBOOLE_1:16
.= ((dom f) /\ (dom g)) /\ (B /\ B) by XBOOLE_1:16 ;
then A18: dom ((f | B) + (g | B)) = (((dom f) /\ (dom g)) /\ B) \ ((((f | B) " {-infty }) /\ ((g | B) " {+infty })) \/ (((f | B) " {+infty }) /\ ((g | B) " {-infty }))) by MESFUNC1:def 3
.= (((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })))) /\ B by A17, XBOOLE_1:50
.= (dom (f + g)) /\ B by MESFUNC1:def 3
.= B by A1, XBOOLE_1:28 ;

now

let x be set ; :: thesis: ( x in dom ((f + g) | B) implies ((f + g) | B) . x = ((f | B) + (g | B)) . x )
assume A19: x in dom ((f + g) | B) ; :: thesis: ((f + g) | B) . x = ((f | B) + (g | B)) . x
hence ((f + g) | B) . x = (f + g) . x by FUNCT_1:70
.= (f . x) + (g . x) by A1, A3, A19, MESFUNC1:def 3
.= ((f | B) . x) + (g . x) by A3, A19, FUNCT_1:70
.= ((f | B) . x) + ((g | B) . x) by A3, A19, FUNCT_1:70
.= ((f | B) + (g | B)) . x by A3, A18, A19, MESFUNC1:def 3 ;
:: thesis: verum

end;

hence ( dom ((f + g) | B) = B & dom ((f | B) + (g | B)) = B & (f + g) | B = (f | B) + (g | B) ) by A3, A18, FUNCT_1:9; :: thesis: verum