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;
now :: thesis: for x being object st x in (g " {+infty}) /\ B holds
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;
then A6: (g " {+infty}) /\ B c= (g | B) " {+infty} ;
now :: thesis: for x being object st x in (g | B) " {+infty} holds
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;
then (g | B) " {+infty} c= (g " {+infty}) /\ B ;
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}
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;
then A17: (g " {-infty}) /\ B c= (g | B) " {-infty} ;
now :: thesis: for x being object st x in (g | B) " {-infty} holds
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;
then (g | B) " {-infty} c= (g " {-infty}) /\ B ;
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}
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;
then A28: (f " {+infty}) /\ B c= (f | B) " {+infty} ;
now :: thesis: for x being object st x in (f " {-infty}) /\ B holds
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;
then A33: (f " {-infty}) /\ B c= (f | B) " {-infty} ;
now :: thesis: for x being object st x in (f | B) " {-infty} holds
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;
then (f | B) " {-infty} c= (f " {-infty}) /\ B ;
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
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;
then (f | B) " {+infty} c= (f " {+infty}) /\ B ;
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
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;
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