let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f)
let f be PartFunc of X,REAL; :: thesis: |.(R_EAL f).| = R_EAL (abs f)
A1: now :: thesis: for x being Element of X st x in dom |.(R_EAL f).| holds
|.(R_EAL f).| . x = (R_EAL (abs f)) . x
let x be Element of X; :: thesis: ( x in dom |.(R_EAL f).| implies |.(R_EAL f).| . x = (R_EAL (abs f)) . x )
assume x in dom |.(R_EAL f).| ; :: thesis: |.(R_EAL f).| . x = (R_EAL (abs f)) . x
then |.(R_EAL f).| . x = |.((R_EAL f) . x).| by MESFUNC1:def 10;
then |.(R_EAL f).| . x = |.(f . x).| by EXTREAL1:12;
then |.(R_EAL f).| . x = |.f.| . x by VALUED_1:18;
hence |.(R_EAL f).| . x = (R_EAL (abs f)) . x ; :: thesis: verum
end;
dom |.(R_EAL f).| = dom (R_EAL f) by MESFUNC1:def 10
.= dom (abs f) by VALUED_1:def 11 ;
hence |.(R_EAL f).| = R_EAL (abs f) by A1, PARTFUN1:5; :: thesis: verum