let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
let f, g be PartFunc of X,ExtREAL; :: thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
A1: |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| by Th18;
A2: dom |.(f + g).| c= dom |.g.| by Th19;
then A3: dom |.(f + g).| c= dom g by MESFUNC1:def 10;
dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) by RELAT_1:61;
then A4: dom (g | (dom |.(f + g).|)) = dom |.(f + g).| by A3, XBOOLE_1:28;
then A5: dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| by MESFUNC1:def 10;
A6: dom |.(f + g).| c= dom |.f.| by Th19;
then A7: dom |.(f + g).| c= dom f by MESFUNC1:def 10;
then (dom |.(f + g).|) /\ (dom |.(f + g).|) c= (dom f) /\ (dom g) by A3, XBOOLE_1:27;
then A8: dom |.(f + g).| c= dom (|.f.| + |.g.|) by Th19;
then A9: 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 A10: dom (f | (dom |.(f + g).|)) = dom |.(f + g).| by A7, XBOOLE_1:28;
A11: |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| by Th18;
then A12: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by A1, Th19
.= dom |.(f + g).| by A10, A4 ;
A13: dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| by A10, MESFUNC1:def 10;

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 A14: 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 A15: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:47
.= (|.f.| . x) + (|.g.| . x) by A8, A9, A14, MESFUNC1:def 3
.= |.(f . x).| + (|.g.| . x) by A6, A9, A14, MESFUNC1:def 10 ;
A16: x in dom |.(f + g).| by A8, A14, RELAT_1:62;
then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A12, MESFUNC1:def 3
.= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A13, A11, A1, A16, MESFUNC1:def 10
.= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A5, A16, MESFUNC1:def 10
.= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A16, FUNCT_1:49
.= |.(f . x).| + |.(g . x).| by A16, FUNCT_1:49 ;
hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A2, A9, A14, A15, MESFUNC1:def 10; :: thesis: verum

end;

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