let n be Nat; :: thesis: for Z, x being set
for f being PartFunc of Z,(REAL n)
for r being Real st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
let Z, x be set ; :: thesis: for f being PartFunc of Z,(REAL n)
for r being Real st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
let f be PartFunc of Z,(REAL n); :: thesis: for r being Real st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
let r be Real; :: thesis: ( x in dom (r (#) f) implies (r (#) f) /. x = r * (f /. x) )
assume A1: x in dom (r (#) f) ; :: thesis: (r (#) f) /. x = r * (f /. x)
dom (r (#) f) = dom f by VALUED_2:def 39;
then A2: f . x = f /. x by A1, PARTFUN1:def 6;
thus (r (#) f) /. x = (r (#) f) . x by A1, PARTFUN1:def 6
.= r * (f /. x) by A1, A2, VALUED_2:def 39 ; :: thesis: verum