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 A3: 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, A3, Def3; :: thesis: verum

end;

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