let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for D being set holds abs (f | D) = (abs f) | D
let f be PartFunc of X,REAL ; :: thesis: for D being set holds abs (f | D) = (abs f) | D
let D be set ; :: thesis: abs (f | D) = (abs f) | D
A2: dom (abs (f | D)) = dom (f | D) by VALUED_1:def 11;
then dom (abs (f | D)) = (dom f) /\ D by RELAT_1:90;
then dom (abs (f | D)) = (dom (abs f)) /\ D by VALUED_1:def 11;
then A3: dom (abs (f | D)) = dom ((abs f) | D) by RELAT_1:90;
for x being Element of X st x in dom (abs (f | D)) holds
(abs (f | D)) . x = ((abs f) | D) . x

proof

let x be Element of X; :: thesis: ( x in dom (abs (f | D)) implies (abs (f | D)) . x = ((abs f) | D) . x )
assume B1: x in dom (abs (f | D)) ; :: thesis: (abs (f | D)) . x = ((abs f) | D) . x
then x in dom f by A2, RELAT_1:86;
then B2: x in dom (abs f) by VALUED_1:def 11;
(abs (f | D)) . x = abs ((f | D) . x) by B1, VALUED_1:def 11;
then (abs (f | D)) . x = abs (f . x) by B1, A2, FUNCT_1:70;
then (abs (f | D)) . x = (abs f) . x by B2, VALUED_1:def 11;
hence (abs (f | D)) . x = ((abs f) | D) . x by B1, A3, FUNCT_1:70; :: thesis: verum

end;

hence abs (f | D) = (abs f) | D by A3, PARTFUN1:34; :: thesis: verum