let X, Y be non empty set ; 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; ( 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
; ( 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;
hence
f1 + f2 = f1
by A4, A1, A3, XBOOLE_1:28, PARTFUN1:5; ( f1 - f2 = f1 & f2 - f1 = - f1 )
hence
f1 - f2 = f1
by A4, A1, A3, XBOOLE_1:28, PARTFUN1:5; f2 - f1 = - f1
hence
f2 - f1 = - f1
by A6, PARTFUN1:5; verum