let X be non empty set ; 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; (|.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 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).|))) . xlet x be
Element of
X;
( 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).|))
;
((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . xthen 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;
verum end;
hence
(|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
by A12, A8, PARTFUN1:5, RELAT_1:62; verum