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