let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let f, g be PartFunc of X,ExtREAL; :: thesis: for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let x be set ; :: thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x )
A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;
assume A2: x in dom |.(f + g).| ; :: thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x
then x in dom (f + g) by MESFUNC1:def 10;
then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A1, MESFUNC1:def 3;
A4: dom |.(f + g).| c= dom |.g.| by Th19;
then A5: |.(g . x).| = |.g.| . x by A2, MESFUNC1:def 10;
x in dom |.g.| by A2, A4;
then A6: x in dom g by MESFUNC1:def 10;
A7: dom |.(f + g).| c= dom |.f.| by Th19;
then x in dom |.f.| by A2;
then x in dom f by MESFUNC1:def 10;
then x in (dom f) /\ (dom g) by A6, XBOOLE_0:def 4;
then A8: x in dom (|.f.| + |.g.|) by Th19;
|.(f . x).| = |.f.| . x by A2, A7, MESFUNC1:def 10;
then |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A5, A8, MESFUNC1:def 3;
hence |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, MESFUNC1:def 10; :: thesis: verum