let X be non empty set ; :: thesis: for f1 being without-infty Function of X,ExtREAL
for f2 being without+infty Function of X,ExtREAL holds
( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) & - (f1 - f2) = (- f1) + f2 & - (f2 - f1) = (- f2) + f1 )
let f1 be without-infty Function of X,ExtREAL; :: thesis: for f2 being without+infty Function of X,ExtREAL holds
( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) & - (f1 - f2) = (- f1) + f2 & - (f2 - f1) = (- f2) + f1 )
let f2 be without+infty Function of X,ExtREAL; :: thesis: ( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) & - (f1 - f2) = (- f1) + f2 & - (f2 - f1) = (- f2) + f1 )
thus A1: ( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) ) by Lm5; :: thesis: ( - (f1 - f2) = (- f1) + f2 & - (f2 - f1) = (- f2) + f1 )
thus - (f1 - f2) = (- f1) - (- f2) by A1, Th8
.= (- f1) + (- (- f2)) by Lm5
.= (- f1) + f2 by Th2 ; :: thesis: - (f2 - f1) = (- f2) + f1
thus - (f2 - f1) = (- f2) - (- f1) by A1, Th9
.= (- f2) + (- (- f1)) by Lm5
.= (- f2) + f1 by Th2 ; :: thesis: verum