let X, Y be non empty set ; :: thesis: for f1, f2 being PartFunc of X,ExtREAL st dom f1 c= Y & f2 = Y --> 0 holds
( f1 + f2 = f1 & f1 - f2 = f1 & f2 - f1 = - f1 )
let f1, f2 be PartFunc of X,ExtREAL; :: thesis: ( dom f1 c= Y & f2 = Y --> 0 implies ( f1 + f2 = f1 & f1 - f2 = f1 & f2 - f1 = - f1 ) )
assume that
A1: dom f1 c= Y and
A2: f2 = Y --> 0 ; :: thesis: ( f1 + f2 = f1 & f1 - f2 = f1 & f2 - f1 = - f1 )
A3: dom f2 = Y by A2, FUNCOP_1:13;
( f2 is V120() & f2 is V121() ) by A2, Th21;
then A4: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & dom (f1 - f2) = (dom f1) /\ (dom f2) & dom (f2 - f1) = (dom f1) /\ (dom f2) ) by Th23;
then A5: ( dom (f1 + f2) = dom f1 & dom (f1 - f2) = dom f1 & dom (f2 - f1) = dom f1 ) by A1, A3, XBOOLE_1:28;
then A6: dom (- f1) = dom (f2 - f1) by MESFUNC1:def 7;
now :: thesis: for x being Element of X st x in dom (f1 + f2) holds
(f1 + f2) . x = f1 . x
let x be Element of X; :: thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = f1 . x )
assume A7: x in dom (f1 + f2) ; :: thesis: (f1 + f2) . x = f1 . x
then A8: f2 . x = 0 by A1, A2, A5, FUNCOP_1:7;
(f1 + f2) . x = (f1 . x) + (f2 . x) by A7, MESFUNC1:def 3;
hence (f1 + f2) . x = f1 . x by A8, XXREAL_3:4; :: thesis: verum
end;
hence f1 + f2 = f1 by A4, A1, A3, XBOOLE_1:28, PARTFUN1:5; :: thesis: ( f1 - f2 = f1 & f2 - f1 = - f1 )
now :: thesis: for x being Element of X st x in dom (f1 - f2) holds
(f1 - f2) . x = f1 . x
let x be Element of X; :: thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = f1 . x )
assume A9: x in dom (f1 - f2) ; :: thesis: (f1 - f2) . x = f1 . x
then A10: f2 . x = 0 by A1, A2, A5, FUNCOP_1:7;
(f1 - f2) . x = (f1 . x) - (f2 . x) by A9, MESFUNC1:def 4;
hence (f1 - f2) . x = f1 . x by A10, XXREAL_3:15; :: thesis: verum
end;
hence f1 - f2 = f1 by A4, A1, A3, XBOOLE_1:28, PARTFUN1:5; :: thesis: f2 - f1 = - f1
now :: thesis: for x being Element of X st x in dom (f2 - f1) holds
(f2 - f1) . x = (- f1) . x
let x be Element of X; :: thesis: ( x in dom (f2 - f1) implies (f2 - f1) . x = (- f1) . x )
assume A11: x in dom (f2 - f1) ; :: thesis: (f2 - f1) . x = (- f1) . x
then A12: f2 . x = 0 by A1, A2, A5, FUNCOP_1:7;
(f2 - f1) . x = (f2 . x) - (f1 . x) by A11, MESFUNC1:def 4
.= (- (f1 . x)) + (f2 . x) by XXREAL_3:def 4
.= - (f1 . x) by A12, XXREAL_3:4 ;
hence (f2 - f1) . x = (- f1) . x by A11, A6, MESFUNC1:def 7; :: thesis: verum
end;
hence f2 - f1 = - f1 by A6, PARTFUN1:5; :: thesis: verum