let f be complex-valued Function; :: thesis: for x being object holds f . x = ((delneg f) . x) - ((delpos f) . x)
let x be object ; :: thesis: f . x = ((delneg f) . x) - ((delpos f) . x)
K1: ( dom (delneg f) = dom f & dom (delpos f) = dom f ) by DMN;
per cases ( not x in dom f or x in dom f ) ;
suppose not x in dom f ; :: thesis: f . x = ((delneg f) . x) - ((delpos f) . x)
then ( f . x = {} & (delneg f) . x = {} & (delpos f) . x = {} ) by K1, FUNCT_1:def 2;
hence f . x = ((delneg f) . x) - ((delpos f) . x) ; :: thesis: verum
end;
suppose A1: x in dom f ; :: thesis: f . x = ((delneg f) . x) - ((delpos f) . x)
per cases ( f is empty or not f is empty ) ;
suppose B1: f is empty ; :: thesis: f . x = ((delneg f) . x) - ((delpos f) . x)
then ( (1 / 2) (#) (f + (abs f)) is empty & (1 / 2) (#) ((abs f) - f) is empty ) ;
hence f . x = ((delneg f) . x) - ((delpos f) . x) by B1; :: thesis: verum
end;
suppose not f is empty ; :: thesis: f . x = ((delneg f) . x) - ((delpos f) . x)
then reconsider X = dom f as non empty set ;
reconsider f = f as X -defined total complex-valued Function by RELAT_1:def 18, PARTFUN1:def 2;
A2: dom ((delneg f) - (delpos f)) = (dom (delneg f)) /\ (dom (delpos f)) by VALUED_1:12
.= (dom f) /\ (dom (delpos f)) by DMN
.= (dom f) /\ (dom f) by DMN
.= dom f ;
f . x = (((1 / 2) + (1 / 2)) (#) f) . x
.= ((((1 / 2) (#) f) + (((1 / 2) (#) (abs f)) - ((1 / 2) (#) (abs f)))) + ((1 / 2) (#) f)) . x by TOPREALC:2
.= (((((1 / 2) (#) f) + ((1 / 2) (#) (abs f))) - ((1 / 2) (#) (abs f))) + ((1 / 2) (#) f)) . x by RFUNCT_1:23
.= ((((1 / 2) (#) f) + ((1 / 2) (#) (abs f))) - (((1 / 2) (#) (abs f)) - ((1 / 2) (#) f))) . x by RFUNCT_1:22
.= ((delneg f) - (((1 / 2) (#) (abs f)) - ((1 / 2) (#) f))) . x by RFUNCT_1:16
.= ((delneg f) - (delpos f)) . x by RFUNCT_1:18
.= ((delneg f) . x) - ((delpos f) . x) by A1, A2, VALUED_1:13 ;
hence f . x = ((delneg f) . x) - ((delpos f) . x) ; :: thesis: verum
end;
end;
end;
end;