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

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