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

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:34; :: thesis: verum