let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for f0 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for x0 being Element of (REAL-NS m) st x in dom f & x = x0 & f = f0 holds
f /. x = f0 /. x0
let f be PartFunc of (REAL m),(REAL n); :: thesis: for f0 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for x0 being Element of (REAL-NS m) st x in dom f & x = x0 & f = f0 holds
f /. x = f0 /. x0
let f0 be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Element of REAL m
for x0 being Element of (REAL-NS m) st x in dom f & x = x0 & f = f0 holds
f /. x = f0 /. x0
let x be Element of REAL m; :: thesis: for x0 being Element of (REAL-NS m) st x in dom f & x = x0 & f = f0 holds
f /. x = f0 /. x0
let x0 be Element of (REAL-NS m); :: thesis: ( x in dom f & x = x0 & f = f0 implies f /. x = f0 /. x0 )
assume A1: ( x in dom f & x = x0 & f = f0 ) ; :: thesis: f /. x = f0 /. x0
then f /. x = f0 . x0 by PARTFUN1:def 6;
hence f /. x = f0 /. x0 by A1, PARTFUN1:def 6; :: thesis: verum