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 object st x in dom g holds

g . x in ExtREAL by XXREAL_0:def 1;

then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:3;

for x being object st x in dom (g | B) holds

(g | B) . x in ExtREAL by XXREAL_0:def 1;

then reconsider gb = g | B as Function of (dom (g | B)),ExtREAL by FUNCT_2:3;

then A12: (g | B) " {+infty} = (g " {+infty}) /\ B by A6;

then A23: (g | B) " {-infty} = (g " {-infty}) /\ B by A17;

for x being object st x in dom f holds

f . x in ExtREAL by XXREAL_0:def 1;

then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:3;

for x being object st x in dom (f | B) holds

(f | B) . x in ExtREAL by XXREAL_0:def 1;

then reconsider fb = f | B as Function of (dom (f | B)),ExtREAL by FUNCT_2:3;

then (f | B) " {-infty} = (f " {-infty}) /\ B by A33;

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 ;

then (f | B) " {+infty} = (f " {+infty}) /\ B by A28;

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:61

.= ((dom f) /\ B) /\ ((dom g) /\ B) by RELAT_1:61

.= (((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;

dom (g | B) = (dom g) /\ B by RELAT_1:61;

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:61;

then A50: dom ((f + g) | B) = B by A1, XBOOLE_1:28;

dom (f | B) = (dom f) /\ B by RELAT_1:61;

then A51: dom (f | B) = B by A47, XBOOLE_1:18, XBOOLE_1:28;

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 object st x in dom g holds

g . x in ExtREAL by XXREAL_0:def 1;

then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:3;

for x being object st x in dom (g | B) holds

(g | B) . x in ExtREAL by XXREAL_0:def 1;

then reconsider gb = g | B as Function of (dom (g | B)),ExtREAL by FUNCT_2:3;

now :: thesis: for x being object st x in (g " {+infty}) /\ B holds

x in (g | B) " {+infty}

then A6:
(g " {+infty}) /\ B c= (g | B) " {+infty}
;x in (g | B) " {+infty}

let x be object ; :: 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:38;

then x in (dom gg) /\ B by A3, XBOOLE_0:def 4;

then A5: x in dom (gg | B) by RELAT_1:61;

gg . x in {+infty} by A4, FUNCT_2:38;

then gb . x in {+infty} by A5, FUNCT_1:47;

hence x in (g | B) " {+infty} by A5, FUNCT_2:38; :: thesis: verum

end;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:38;

then x in (dom gg) /\ B by A3, XBOOLE_0:def 4;

then A5: x in dom (gg | B) by RELAT_1:61;

gg . x in {+infty} by A4, FUNCT_2:38;

then gb . x in {+infty} by A5, FUNCT_1:47;

hence x in (g | B) " {+infty} by A5, FUNCT_2:38; :: thesis: verum

now :: thesis: for x being object st x in (g | B) " {+infty} holds

x in (g " {+infty}) /\ B

then
(g | B) " {+infty} c= (g " {+infty}) /\ B
;x in (g " {+infty}) /\ B

let x be object ; :: 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:38;

then A9: x in (dom g) /\ B by RELAT_1:61;

then A10: x in dom g by XBOOLE_0:def 4;

gb . x in {+infty} by A7, FUNCT_2:38;

then g . x in {+infty} by A8, FUNCT_1:47;

then A11: x in gg " {+infty} by A10, FUNCT_2:38;

x in B by A9, XBOOLE_0:def 4;

hence x in (g " {+infty}) /\ B by A11, XBOOLE_0:def 4; :: thesis: verum

end;assume A7: x in (g | B) " {+infty} ; :: thesis: x in (g " {+infty}) /\ B

then A8: x in dom gb by FUNCT_2:38;

then A9: x in (dom g) /\ B by RELAT_1:61;

then A10: x in dom g by XBOOLE_0:def 4;

gb . x in {+infty} by A7, FUNCT_2:38;

then g . x in {+infty} by A8, FUNCT_1:47;

then A11: x in gg " {+infty} by A10, FUNCT_2:38;

x in B by A9, XBOOLE_0:def 4;

hence x in (g " {+infty}) /\ B by A11, XBOOLE_0:def 4; :: thesis: verum

then A12: (g | B) " {+infty} = (g " {+infty}) /\ B by A6;

now :: thesis: for x being object st x in (g " {-infty}) /\ B holds

x in (g | B) " {-infty}

then A17:
(g " {-infty}) /\ B c= (g | B) " {-infty}
;x in (g | B) " {-infty}

let x be object ; :: 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:38;

then x in (dom gg) /\ B by A14, XBOOLE_0:def 4;

then A16: x in dom (gg | B) by RELAT_1:61;

gg . x in {-infty} by A15, FUNCT_2:38;

then gb . x in {-infty} by A16, FUNCT_1:47;

hence x in (g | B) " {-infty} by A16, FUNCT_2:38; :: thesis: verum

end;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:38;

then x in (dom gg) /\ B by A14, XBOOLE_0:def 4;

then A16: x in dom (gg | B) by RELAT_1:61;

gg . x in {-infty} by A15, FUNCT_2:38;

then gb . x in {-infty} by A16, FUNCT_1:47;

hence x in (g | B) " {-infty} by A16, FUNCT_2:38; :: thesis: verum

now :: thesis: for x being object st x in (g | B) " {-infty} holds

x in (g " {-infty}) /\ B

then
(g | B) " {-infty} c= (g " {-infty}) /\ B
;x in (g " {-infty}) /\ B

let x be object ; :: 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:38;

then A20: x in (dom g) /\ B by RELAT_1:61;

then A21: x in dom g by XBOOLE_0:def 4;

gb . x in {-infty} by A18, FUNCT_2:38;

then g . x in {-infty} by A19, FUNCT_1:47;

then A22: x in gg " {-infty} by A21, FUNCT_2:38;

x in B by A20, XBOOLE_0:def 4;

hence x in (g " {-infty}) /\ B by A22, XBOOLE_0:def 4; :: thesis: verum

end;assume A18: x in (g | B) " {-infty} ; :: thesis: x in (g " {-infty}) /\ B

then A19: x in dom gb by FUNCT_2:38;

then A20: x in (dom g) /\ B by RELAT_1:61;

then A21: x in dom g by XBOOLE_0:def 4;

gb . x in {-infty} by A18, FUNCT_2:38;

then g . x in {-infty} by A19, FUNCT_1:47;

then A22: x in gg " {-infty} by A21, FUNCT_2:38;

x in B by A20, XBOOLE_0:def 4;

hence x in (g " {-infty}) /\ B by A22, XBOOLE_0:def 4; :: thesis: verum

then A23: (g | B) " {-infty} = (g " {-infty}) /\ B by A17;

for x being object st x in dom f holds

f . x in ExtREAL by XXREAL_0:def 1;

then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:3;

for x being object st x in dom (f | B) holds

(f | B) . x in ExtREAL by XXREAL_0:def 1;

then reconsider fb = f | B as Function of (dom (f | B)),ExtREAL by FUNCT_2:3;

now :: thesis: for x being object st x in (f " {+infty}) /\ B holds

x in (f | B) " {+infty}

then A28:
(f " {+infty}) /\ B c= (f | B) " {+infty}
;x in (f | B) " {+infty}

let x be object ; :: 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:38;

then x in (dom ff) /\ B by A25, XBOOLE_0:def 4;

then A27: x in dom (ff | B) by RELAT_1:61;

ff . x in {+infty} by A26, FUNCT_2:38;

then fb . x in {+infty} by A27, FUNCT_1:47;

hence x in (f | B) " {+infty} by A27, FUNCT_2:38; :: thesis: verum

end;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:38;

then x in (dom ff) /\ B by A25, XBOOLE_0:def 4;

then A27: x in dom (ff | B) by RELAT_1:61;

ff . x in {+infty} by A26, FUNCT_2:38;

then fb . x in {+infty} by A27, FUNCT_1:47;

hence x in (f | B) " {+infty} by A27, FUNCT_2:38; :: thesis: verum

now :: thesis: for x being object st x in (f " {-infty}) /\ B holds

x in (f | B) " {-infty}

then A33:
(f " {-infty}) /\ B c= (f | B) " {-infty}
;x in (f | B) " {-infty}

let x be object ; :: 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:38;

then x in (dom ff) /\ B by A30, XBOOLE_0:def 4;

then A32: x in dom (ff | B) by RELAT_1:61;

ff . x in {-infty} by A31, FUNCT_2:38;

then fb . x in {-infty} by A32, FUNCT_1:47;

hence x in (f | B) " {-infty} by A32, FUNCT_2:38; :: thesis: verum

end;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:38;

then x in (dom ff) /\ B by A30, XBOOLE_0:def 4;

then A32: x in dom (ff | B) by RELAT_1:61;

ff . x in {-infty} by A31, FUNCT_2:38;

then fb . x in {-infty} by A32, FUNCT_1:47;

hence x in (f | B) " {-infty} by A32, FUNCT_2:38; :: thesis: verum

now :: thesis: for x being object st x in (f | B) " {-infty} holds

x in (f " {-infty}) /\ B

then
(f | B) " {-infty} c= (f " {-infty}) /\ B
;x in (f " {-infty}) /\ B

let x be object ; :: 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:38;

then A36: x in (dom f) /\ B by RELAT_1:61;

then A37: x in dom f by XBOOLE_0:def 4;

fb . x in {-infty} by A34, FUNCT_2:38;

then f . x in {-infty} by A35, FUNCT_1:47;

then A38: x in ff " {-infty} by A37, FUNCT_2:38;

x in B by A36, XBOOLE_0:def 4;

hence x in (f " {-infty}) /\ B by A38, XBOOLE_0:def 4; :: thesis: verum

end;assume A34: x in (f | B) " {-infty} ; :: thesis: x in (f " {-infty}) /\ B

then A35: x in dom fb by FUNCT_2:38;

then A36: x in (dom f) /\ B by RELAT_1:61;

then A37: x in dom f by XBOOLE_0:def 4;

fb . x in {-infty} by A34, FUNCT_2:38;

then f . x in {-infty} by A35, FUNCT_1:47;

then A38: x in ff " {-infty} by A37, FUNCT_2:38;

x in B by A36, XBOOLE_0:def 4;

hence x in (f " {-infty}) /\ B by A38, XBOOLE_0:def 4; :: thesis: verum

then (f | B) " {-infty} = (f " {-infty}) /\ B by A33;

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 :: thesis: for x being object st x in (f | B) " {+infty} holds

x in (f " {+infty}) /\ B

then
(f | B) " {+infty} c= (f " {+infty}) /\ B
;x in (f " {+infty}) /\ B

let x be object ; :: 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:38;

then A42: x in (dom f) /\ B by RELAT_1:61;

then A43: x in dom f by XBOOLE_0:def 4;

fb . x in {+infty} by A40, FUNCT_2:38;

then f . x in {+infty} by A41, FUNCT_1:47;

then A44: x in ff " {+infty} by A43, FUNCT_2:38;

x in B by A42, XBOOLE_0:def 4;

hence x in (f " {+infty}) /\ B by A44, XBOOLE_0:def 4; :: thesis: verum

end;assume A40: x in (f | B) " {+infty} ; :: thesis: x in (f " {+infty}) /\ B

then A41: x in dom fb by FUNCT_2:38;

then A42: x in (dom f) /\ B by RELAT_1:61;

then A43: x in dom f by XBOOLE_0:def 4;

fb . x in {+infty} by A40, FUNCT_2:38;

then f . x in {+infty} by A41, FUNCT_1:47;

then A44: x in ff " {+infty} by A43, FUNCT_2:38;

x in B by A42, XBOOLE_0:def 4;

hence x in (f " {+infty}) /\ B by A44, XBOOLE_0:def 4; :: thesis: verum

then (f | B) " {+infty} = (f " {+infty}) /\ B by A28;

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:61

.= ((dom f) /\ B) /\ ((dom g) /\ B) by RELAT_1:61

.= (((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;

dom (g | B) = (dom g) /\ B by RELAT_1:61;

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:61;

then A50: dom ((f + g) | B) = B by A1, XBOOLE_1:28;

dom (f | B) = (dom f) /\ B by RELAT_1:61;

then A51: dom (f | B) = B by A47, XBOOLE_1:18, XBOOLE_1:28;

now :: thesis: for x being object st x in dom ((f + g) | B) holds

((f + g) | B) . x = ((f | B) + (g | B)) . x

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:2, XBOOLE_1:28; :: thesis: verum((f + g) | B) . x = ((f | B) + (g | B)) . x

let x be object ; :: 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:47

.= (f . x) + (g . x) by A1, A50, A52, MESFUNC1:def 3

.= ((f | B) . x) + (g . x) by A50, A51, A52, FUNCT_1:47

.= ((f | B) . x) + ((g | B) . x) by A50, A48, A52, FUNCT_1:47

.= ((f | B) + (g | B)) . x by A50, A46, A52, MESFUNC1:def 3 ;

:: thesis: verum

end;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:47

.= (f . x) + (g . x) by A1, A50, A52, MESFUNC1:def 3

.= ((f | B) . x) + (g . x) by A50, A51, A52, FUNCT_1:47

.= ((f | B) . x) + ((g | B) . x) by A50, A48, A52, FUNCT_1:47

.= ((f | B) + (g | B)) . x by A50, A46, A52, MESFUNC1:def 3 ;

:: thesis: verum