let n be Nat; :: thesis: for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)
let Z, x be set ; :: thesis: for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)
let f, g be PartFunc of Z,(REAL n); :: thesis: ( x in dom (f - g) implies (f - g) /. x = (f /. x) - (g /. x) )
assume A1: x in dom (f - g) ; :: thesis: (f - g) /. x = (f /. x) - (g /. x)
dom (f - g) = (dom f) /\ (dom g) by VALUED_2:def 46;
then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def 4;
then A2: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def 6;
thus (f - g) /. x = (f - g) . x by A1, PARTFUN1:def 6
.= (f /. x) - (g /. x) by A1, A2, VALUED_2:def 46 ; :: thesis: verum