let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
let f, g be PartFunc of X,COMPLEX ; :: thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
A1: ( dom |.(f + g).| c= dom |.f.| & dom |.(f + g).| c= dom |.g.| ) by Th19;
then A2: ( dom |.(f + g).| c= dom f & dom |.(f + g).| c= dom g ) by VALUED_1:def 11;
( dom (f | (dom |.(f + g).|)) = (dom f) /\ (dom |.(f + g).|) & dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) ) by RELAT_1:90;
then A3: ( dom (f | (dom |.(f + g).|)) = dom |.(f + g).| & dom (g | (dom |.(f + g).|)) = dom |.(f + g).| ) by A2, XBOOLE_1:28;
then A4: ( dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| & dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| ) by VALUED_1:def 11;
A5: ( |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| & |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| ) by Th18;
then A6: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by Th19
.= dom |.(f + g).| by A3 ;
(dom |.(f + g).|) /\ (dom |.(f + g).|) c= (dom f) /\ (dom g) by A2, XBOOLE_1:27;
then A7: dom |.(f + g).| c= dom (|.f.| + |.g.|) by Th19;
then A8: dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) = dom |.(f + g).| by RELAT_1:91;

now

let x be Element of X; :: thesis: ( x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) implies ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x )
assume A9: x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) ; :: thesis: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x
then A10: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:70
.= (|.f.| . x) + (|.g.| . x) by A7, A8, A9, VALUED_1:def 1
.= |.(f . x).| + (|.g.| . x) by A1, A8, A9, VALUED_1:def 11 ;
A11: x in dom |.(f + g).| by A7, A9, RELAT_1:91;
then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A6, VALUED_1:def 1
.= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A4, A5, A11, VALUED_1:def 11
.= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A4, A11, VALUED_1:def 11
.= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A11, FUNCT_1:72
.= |.(f . x).| + |.(g . x).| by A11, FUNCT_1:72 ;
hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A1, A8, A9, A10, VALUED_1:def 11; :: thesis: verum

end;

hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A6, A7, PARTFUN1:34, RELAT_1:91; :: thesis: verum