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 ;
then A4: x in dom (abs f) by VALUED_1:def 11;
(abs (f | D)) . x = |.((f | D) . x).| by ;
then (abs (f | D)) . x = |.(f . x).| by ;
then (abs (f | D)) . x = (abs f) . x by ;
hence (abs (f | D)) . x = ((abs f) | D) . x by ; :: thesis: verum
end;
hence abs (f | D) = (abs f) | D by ; :: thesis: verum