let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = () | (dom |.(f + g).|)
let f, g be PartFunc of X,COMPLEX; :: thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(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 ;
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 ;
then A7: dom |.(f + g).| c= dom () by Th38;
then A8: dom (() | (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 ;
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 ;
now :: thesis: for x being Element of X st x in dom (() | (dom |.(f + g).|)) holds
(() | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x
let x be Element of X; :: thesis: ( x in dom (() | (dom |.(f + g).|)) implies (() | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x )
assume A13: x in dom (() | (dom |.(f + g).|)) ; :: thesis: (() | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x
then A14: (() | (dom |.(f + g).|)) . x = () . x by FUNCT_1:47
.= (|.f.| . x) + (|.g.| . x) by
.= |.(f . x).| + (|.g.| . x) by ;
A15: x in dom |.(f + g).| by ;
then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by
.= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by
.= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by
.= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by
.= |.(f . x).| + |.(g . x).| by ;
hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by ; :: thesis: verum
end;
hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = () | (dom |.(f + g).|) by ; :: thesis: verum