let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r being Real
for X being set holds (F | X) - r = (F - r) | X
let F be PartFunc of D,REAL ; :: thesis: for r being Real
for X being set holds (F | X) - r = (F - r) | X
let r be Real; :: thesis: for X being set holds (F | X) - r = (F - r) | X
let X be set ; :: thesis: (F | X) - r = (F - r) | X
A1: dom ((F | X) - r) = dom (F | X) by VALUED_1:3;
A2: dom (F | X) = (dom F) /\ X by RELAT_1:90;
A3: (dom F) /\ X = (dom (F - r)) /\ X by VALUED_1:3
.= dom ((F - r) | X) by RELAT_1:90 ;

now

let d be Element of D; :: thesis: ( d in dom ((F | X) - r) implies ((F | X) - r) . d = ((F - r) | X) . d )
assume A4: d in dom ((F | X) - r) ; :: thesis: ((F | X) - r) . d = ((F - r) | X) . d
then A5: d in dom F by A1, A2, XBOOLE_0:def 4;
thus ((F | X) - r) . d = ((F | X) . d) - r by A1, A4, VALUED_1:3
.= (F . d) - r by A1, A4, FUNCT_1:70
.= (F - r) . d by A5, VALUED_1:3
.= ((F - r) | X) . d by A1, A2, A3, A4, FUNCT_1:70 ; :: thesis: verum

end;

hence (F | X) - r = (F - r) | X by A2, A3, PARTFUN1:34, VALUED_1:3; :: thesis: verum