let X be set ; :: thesis: for f1, f2 being PartFunc of X,REAL st dom f1 = dom f2 holds
( (f1 + f2) - f2 = f1 & (f1 - f2) + f2 = f1 )
let f1, f2 be PartFunc of X,REAL; :: thesis: ( dom f1 = dom f2 implies ( (f1 + f2) - f2 = f1 & (f1 - f2) + f2 = f1 ) )
assume A1: dom f1 = dom f2 ; :: thesis: ( (f1 + f2) - f2 = f1 & (f1 - f2) + f2 = f1 )
A2: dom (f1 + f2) = (dom f1) /\ (dom f1) by A1, VALUED_1:def 1
.= dom f1 ;
then A3: dom ((f1 + f2) - f2) = (dom f1) /\ (dom f1) by A1, VALUED_1:12
.= dom f1 ;
A4: dom (f1 - f2) = (dom f1) /\ (dom f1) by A1, VALUED_1:12
.= dom f1 ;
then A5: dom ((f1 - f2) + f2) = (dom f1) /\ (dom f1) by A1, VALUED_1:def 1
.= dom f1 ;
for x being Element of X st x in dom f1 holds
f1 . x = ((f1 + f2) - f2) . x

proof

let x be Element of X; :: thesis: ( x in dom f1 implies f1 . x = ((f1 + f2) - f2) . x )
assume A6: x in dom f1 ; :: thesis: f1 . x = ((f1 + f2) - f2) . x
then ((f1 + f2) - f2) . x = ((f1 + f2) . x) - (f2 . x) by A3, VALUED_1:13
.= ((f1 . x) + (f2 . x)) - (f2 . x) by A6, A2, VALUED_1:def 1 ;
hence f1 . x = ((f1 + f2) - f2) . x ; :: thesis: verum

end;

hence (f1 + f2) - f2 = f1 by A3, PARTFUN1:5; :: thesis: (f1 - f2) + f2 = f1
for x being Element of X st x in dom f1 holds
f1 . x = ((f1 - f2) + f2) . x

proof

let x be Element of X; :: thesis: ( x in dom f1 implies f1 . x = ((f1 - f2) + f2) . x )
assume A7: x in dom f1 ; :: thesis: f1 . x = ((f1 - f2) + f2) . x
then ((f1 - f2) + f2) . x = ((f1 - f2) . x) + (f2 . x) by A5, VALUED_1:def 1
.= ((f1 . x) - (f2 . x)) + (f2 . x) by A4, A7, VALUED_1:13 ;
hence f1 . x = ((f1 - f2) + f2) . x ; :: thesis: verum

end;

hence (f1 - f2) + f2 = f1 by A5, PARTFUN1:5; :: thesis: verum