let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let f be PartFunc of C,V; :: thesis: for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let r be Real; :: thesis: ( r <> 0 implies (r (#) f) " {(0. V)} = f " {(0. V)} )
assume A1: r <> 0 ; :: thesis: (r (#) f) " {(0. V)} = f " {(0. V)}

now :: thesis: for c being Element of C holds
( ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} ) )

let c be Element of C; :: thesis: ( ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} ) )
thus ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) :: thesis: ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} )

proof

assume A2: c in (r (#) f) " {(0. V)} ; :: thesis: c in f " {(0. V)}
then A3: c in dom (r (#) f) by PARTFUN2:26;
(r (#) f) /. c in {(0. V)} by A2, PARTFUN2:26;
then (r (#) f) /. c = 0. V by TARSKI:def 1;
then r * (f /. c) = r * (0. V) by A3, Def4;
then f /. c = 0. V by A1, RLVECT_1:36;
then A4: f /. c in {(0. V)} by TARSKI:def 1;
c in dom f by A3, Def4;
hence c in f " {(0. V)} by A4, PARTFUN2:26; :: thesis: verum

end;

assume A5: c in f " {(0. V)} ; :: thesis: c in (r (#) f) " {(0. V)}
then c in dom f by PARTFUN2:26;
then A6: c in dom (r (#) f) by Def4;
f /. c in {(0. V)} by A5, PARTFUN2:26;
then r * (f /. c) = r * (0. V) by TARSKI:def 1;
then (r (#) f) /. c = 0. V by A6, Def4;
then (r (#) f) /. c in {(0. V)} by TARSKI:def 1;
hence c in (r (#) f) " {(0. V)} by A6, PARTFUN2:26; :: thesis: verum

end;

hence (r (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; :: thesis: verum