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

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

hence
abs (f | D) = (abs f) | D
by A2, PARTFUN1:5; :: thesis: verum
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;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