let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))
let f, g be PartFunc of X,REAL; :: thesis: (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))
(R_EAL f) - (R_EAL g) = R_EAL (f - g) by Th23
.= R_EAL (f + (- g)) ;
hence (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g)) by Th23; :: thesis: verum