let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let f, g be PartFunc of X,COMPLEX; :: 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 COMPLEX1:56;
assume A2: x in dom |.(f + g).| ; :: thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x
then x in dom (f + g) by VALUED_1:def 11;
then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A1, VALUED_1:def 1;
A4: dom |.(f + g).| c= dom |.g.| by Th38;
then A5: |.(g . x).| = |.g.| . x by A2, VALUED_1:def 11;
x in dom |.g.| by A2, A4;
then A6: x in dom g by VALUED_1:def 11;
A7: dom |.(f + g).| c= dom |.f.| by Th38;
then x in dom |.f.| by A2;
then x in dom f by VALUED_1:def 11;
then x in (dom f) /\ (dom g) by A6, XBOOLE_0:def 4;
then A8: x in dom (|.f.| + |.g.|) by Th38;
|.(f . x).| = |.f.| . x by A2, A7, VALUED_1:def 11;
then |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A5, A8, VALUED_1:def 1;
hence |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, VALUED_1:def 11; :: thesis: verum