let D be non empty set ; :: thesis: for F being PartFunc of D,REAL holds F - 0 = F
let F be PartFunc of D,REAL; :: thesis: F - 0 = F

A1: now :: thesis: for d being Element of D st d in dom F holds
(F - 0) . d = F . d

let d be Element of D; :: thesis: ( d in dom F implies (F - 0) . d = F . d )
assume d in dom F ; :: thesis: (F - 0) . d = F . d
hence (F - 0) . d = (F . d) - 0 by VALUED_1:3
.= F . d ;
:: thesis: verum

end;

dom (F - 0) = dom F by VALUED_1:3;
hence F - 0 = F by A1, PARTFUN1:5; :: thesis: verum