let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
let f, g be PartFunc of X,COMPLEX; :: thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def 1;
then dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by VALUED_1:def 11;
hence dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by VALUED_1:def 11; :: thesis: dom |.(f + g).| c= dom |.f.|
dom |.(f + g).| = dom (f + g) by VALUED_1:def 11
.= (dom f) /\ (dom g) by VALUED_1:def 1 ;
then dom |.(f + g).| c= dom f by XBOOLE_1:17;
hence dom |.(f + g).| c= dom |.f.| by VALUED_1:def 11; :: thesis: verum