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 |.g.| by Th38;
then A2: dom |.(f + g).| c= dom g by VALUED_1:def 11;
dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) by RELAT_1:61;
then A3: dom (g | (dom |.(f + g).|)) = dom |.(f + g).| by A2, XBOOLE_1:28;
then A4: dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| by VALUED_1:def 11;
A5: dom |.(f + g).| c= dom |.f.| by Th38;
then A6: dom |.(f + g).| c= dom f by VALUED_1:def 11;
then (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 Th38;
then A8: dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) = dom |.(f + g).| by RELAT_1:62;
dom (f | (dom |.(f + g).|)) = (dom f) /\ (dom |.(f + g).|) by RELAT_1:61;
then A9: dom (f | (dom |.(f + g).|)) = dom |.(f + g).| by A6, XBOOLE_1:28;
A10: ( |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| & |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| ) by Th37;
then A11: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by Th38
.= dom |.(f + g).| by A9, A3 ;
A12: dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| by A9, VALUED_1:def 11;

now :: thesis: for x being Element of X st x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) holds
((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x

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 A13: 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 A14: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:47
.= (|.f.| . x) + (|.g.| . x) by A7, A8, A13, VALUED_1:def 1
.= |.(f . x).| + (|.g.| . x) by A5, A8, A13, VALUED_1:def 11 ;
A15: x in dom |.(f + g).| by A7, A13, RELAT_1:62;
then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A11, VALUED_1:def 1
.= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A12, A10, A15, VALUED_1:def 11
.= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A4, A15, VALUED_1:def 11
.= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A15, FUNCT_1:49
.= |.(f . x).| + |.(g . x).| by A15, FUNCT_1:49 ;
hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A1, A8, A13, A14, VALUED_1:def 11; :: thesis: verum

end;

hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A11, A7, PARTFUN1:5, RELAT_1:62; :: thesis: verum