let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,the carrier of 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,the carrier of V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let f be PartFunc of C,the carrier of 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

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 c in (r (#) f) " {(0. V)} ; :: thesis: c in f " {(0. V)}
then ( c in dom (r (#) f) & (r (#) f) /. c in {(0. V)} ) by PARTFUN2:44;
then ( c in dom (r (#) f) & (r (#) f) /. c = 0. V ) by TARSKI:def 1;
then ( c in dom f & r * (f /. c) = 0. V ) by Def4;
then ( c in dom f & r * (f /. c) = r * (0. V) ) by RLVECT_1:23;
then ( c in dom f & f /. c = 0. V ) by A1, RLVECT_1:50;
then ( c in dom f & f /. c in {(0. V)} ) by TARSKI:def 1;
hence c in f " {(0. V)} by PARTFUN2:44; :: thesis: verum

end;

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

end;

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