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) )
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;
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;

now

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

end;

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

now

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

end;

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

now

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

end;

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

now

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

end;

then (g | B) " {-infty } c= (g " {-infty }) /\ B by TARSKI:def 3;
then A23: (g | B) " {-infty } = (g " {-infty }) /\ B by A17, XBOOLE_0:def 10;
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 (f | B) holds
(f | B) . x in ExtREAL ;
then reconsider fb = f | B as Function of (dom (f | B)),ExtREAL by FUNCT_2:5;

now

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

end;

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

now

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

end;

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

now

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

end;

then (f | B) " {-infty } c= (f " {-infty }) /\ B by TARSKI:def 3;
then (f | B) " {-infty } = (f " {-infty }) /\ B by A33, XBOOLE_0:def 10;
then A39: ((f | B) " {-infty }) /\ ((g | B) " {+infty }) = (((f " {-infty }) /\ B) /\ (g " {+infty })) /\ B by A12, XBOOLE_1:16
.= (((f " {-infty }) /\ (g " {+infty })) /\ B) /\ B by XBOOLE_1:16
.= ((f " {-infty }) /\ (g " {+infty })) /\ (B /\ B) by XBOOLE_1:16 ;

now

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

end;

then (f | B) " {+infty } c= (f " {+infty }) /\ B by TARSKI:def 3;
then (f | B) " {+infty } = (f " {+infty }) /\ B by A28, XBOOLE_0:def 10;
then ((f | B) " {+infty }) /\ ((g | B) " {-infty }) = (((f " {+infty }) /\ B) /\ (g " {-infty })) /\ B by A23, XBOOLE_1:16
.= (((f " {+infty }) /\ (g " {-infty })) /\ B) /\ B by XBOOLE_1:16
.= ((f " {+infty }) /\ (g " {-infty })) /\ (B /\ B) by XBOOLE_1:16 ;
then A45: (((f | B) " {-infty }) /\ ((g | B) " {+infty })) \/ (((f | B) " {+infty }) /\ ((g | B) " {-infty })) = (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) /\ B by A39, 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 A46: 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 A45, XBOOLE_1:50
.= (dom (f + g)) /\ B by MESFUNC1:def 3
.= B by A1, XBOOLE_1:28 ;
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 A47: B c= (dom f) /\ (dom g) by A1, XBOOLE_1:1;
dom (g | B) = (dom g) /\ B by RELAT_1:90;
then A48: dom (g | B) = B by A47, XBOOLE_1:18, XBOOLE_1:28;
A49: dom ((f + g) | B) = (dom (f + g)) /\ B by RELAT_1:90;
then A50: dom ((f + g) | B) = B by A1, XBOOLE_1:28;
dom (f | B) = (dom f) /\ B by RELAT_1:90;
then A51: dom (f | B) = B by A47, XBOOLE_1:18, 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 A52: 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, A50, A52, MESFUNC1:def 3
.= ((f | B) . x) + (g . x) by A50, A51, A52, FUNCT_1:70
.= ((f | B) . x) + ((g | B) . x) by A50, A48, A52, FUNCT_1:70
.= ((f | B) + (g | B)) . x by A50, A46, A52, 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 A1, A49, A46, FUNCT_1:9, XBOOLE_1:28; :: thesis: verum