let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,ExtREAL holds f1 + f2 = f2 + f1
let f1, f2 be PartFunc of C,ExtREAL ; :: thesis: f1 + f2 = f2 + f1
A1: dom (f1 + f2) = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty }) /\ (f2 " {+infty })) \/ ((f1 " {+infty }) /\ (f2 " {-infty }))) by Def3
.= dom (f2 + f1) by Def3 ;
for x being Element of C st x in dom (f1 + f2) holds
(f1 + f2) . x = (f2 + f1) . x

proof

let x be Element of C; :: thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (f2 + f1) . x )
assume A2: x in dom (f1 + f2) ; :: thesis: (f1 + f2) . x = (f2 + f1) . x
then (f1 + f2) . x = (f1 . x) + (f2 . x) by Def3;
hence (f1 + f2) . x = (f2 + f1) . x by A1, A2, Def3; :: thesis: verum

end;

hence f1 + f2 = f2 + f1 by A1, PARTFUN1:34; :: thesis: verum