let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds
( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
let f be PartFunc of X,REAL; :: thesis: ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
dom f = dom ((max+ (R_EAL f)) - (max- (R_EAL f))) by MESFUNC2:17;
then dom f = dom ((R_EAL (max+ f)) - (max- (R_EAL f))) by Th30;
then dom f = dom ((R_EAL (max+ f)) - (R_EAL (max- f))) by Th30;
then dom f = dom (R_EAL ((max+ f) - (max- f))) by Th23;
hence dom f = dom ((max+ f) - (max- f)) ; :: thesis: dom f = dom ((max+ f) + (max- f))
dom f = dom ((max+ (R_EAL f)) + (max- (R_EAL f))) by MESFUNC2:17;
then dom f = dom ((R_EAL (max+ f)) + (max- (R_EAL f))) by Th30;
then dom f = dom ((R_EAL (max+ f)) + (R_EAL (max- f))) by Th30;
then dom f = dom (R_EAL ((max+ f) + (max- f))) by Th23;
hence dom f = dom ((max+ f) + (max- f)) ; :: thesis: verum