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

let x be set ; :: thesis: ( x in dom (R_EAL (abs f)) implies (R_EAL (abs f)) . x = |.(R_EAL f).| . x )
(R_EAL (abs f)) . x = |.(f . x).| by VALUED_1:18;
then A2: (R_EAL (abs f)) . x = |.(R_EAL (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