let X be non empty set ; 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; (|.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 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 A13:
x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|))
;
((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . xthen 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;
verum end;
hence
(|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
by A11, A7, PARTFUN1:5, RELAT_1:62; verum