let X be non empty set ; 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; for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let x be set ; ( 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).|
; |.(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; verum