let n be Nat; 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 ; 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); ( x in dom (f + g) implies (f + g) /. x = (f /. x) + (g /. x) )
assume A1:
x in dom (f + g)
; (f + g) /. x = (f /. x) + (g /. x)
dom (f + g) = (dom f) /\ (dom g)
by VALUED_2:def 45;
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 45
; verum