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
A1: dom (abs (f | D)) = dom (f | D) by VALUED_1:def 11;
then dom (abs (f | D)) = (dom f) /\ D by RELAT_1:61;
then dom (abs (f | D)) = (dom (abs f)) /\ D by VALUED_1:def 11;
then A2: dom (abs (f | D)) = dom ((abs f) | D) by RELAT_1:61;
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 A3: x in dom (abs (f | D)) ; :: thesis: (abs (f | D)) . x = ((abs f) | D) . x
then x in dom f by A1, RELAT_1:57;
then A4: x in dom (abs f) by VALUED_1:def 11;
(abs (f | D)) . x = |.((f | D) . x).| by A3, VALUED_1:def 11;
then (abs (f | D)) . x = |.(f . x).| by A3, A1, FUNCT_1:47;
then (abs (f | D)) . x = (abs f) . x by A4, VALUED_1:def 11;
hence (abs (f | D)) . x = ((abs f) | D) . x by A3, A2, FUNCT_1:47; :: thesis: verum

end;

hence abs (f | D) = (abs f) | D by A2, PARTFUN1:5; :: thesis: verum