now :: thesis: for f1, f2 being Function of X,L holds f1 '+' f2 = f2 '+' f1

let f1, f2 be Function of X,L; :: thesis: f1 '+' f2 = f2 '+' f1

now :: thesis: for o being object st o in X holds
(f1 '+' f2) . o = (f2 '+' f1) . o

let o be object ; :: thesis: ( o in X implies (f1 '+' f2) . o = (f2 '+' f1) . o )
assume o in X ; :: thesis: (f1 '+' f2) . o = (f2 '+' f1) . o
then reconsider x = o as Element of X ;
thus (f1 '+' f2) . o = (f1 . x) + (f2 . x) by defp
.= (f2 '+' f1) . o by defp ; :: thesis: verum

end;

hence f1 '+' f2 = f2 '+' f1 by FUNCT_2:12; :: thesis: verum

end;

hence for f, g being Function of X,L holds f '+' g = g '+' f ; :: thesis: verum