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 <= () . x

let f, g be PartFunc of X,COMPLEX; :: thesis: for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= () . x

let x be set ; :: thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= () . x )
A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by COMPLEX1:56;
assume A2: x in dom |.(f + g).| ; :: thesis: |.(f + g).| . x <= () . x
then x in dom (f + g) by VALUED_1:def 11;
then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by ;
A4: dom |.(f + g).| c= dom |.g.| by Th38;
then A5: |.(g . x).| = |.g.| . x by ;
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 ;
then A8: x in dom () by Th38;
|.(f . x).| = |.f.| . x by ;
then |.(f . x).| + |.(g . x).| = () . x by ;
hence |.(f + g).| . x <= () . x by ; :: thesis: verum