let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).|
let f be PartFunc of X,REAL; :: thesis: R_EAL (abs f) = |.(R_EAL f).|
A1: dom (R_EAL (abs f)) = dom f by VALUED_1:def 11
.= dom |.(R_EAL f).| by MESFUNC1:def 10 ;
now :: thesis: for x being object st x in dom (R_EAL (abs f)) holds
(R_EAL (abs f)) . x = |.(R_EAL f).| . x
let x be object ; :: thesis: ( x in dom (R_EAL (abs f)) implies (R_EAL (abs f)) . x = |.(R_EAL f).| . x )
reconsider fx = f . x as Real ;
(R_EAL (abs f)) . x = |.fx.| by VALUED_1:18;
then A2: (R_EAL (abs f)) . x = |.(f . x).| by Th43;
assume x in dom (R_EAL (abs f)) ; :: thesis: (R_EAL (abs f)) . x = |.(R_EAL f).| . x
hence (R_EAL (abs f)) . x = |.(R_EAL f).| . x by A1, A2, MESFUNC1:def 10; :: thesis: verum
end;
hence R_EAL (abs f) = |.(R_EAL f).| by A1, FUNCT_1:2; :: thesis: verum