let r be Real; :: thesis: for X, Y being non empty set
for V being RealNormSpace
for g being PartFunc of X,the carrier of V
for g1 being PartFunc of Y,the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let X, Y be non empty set ; :: thesis: for V being RealNormSpace
for g being PartFunc of X,the carrier of V
for g1 being PartFunc of Y,the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let V be RealNormSpace; :: thesis: for g being PartFunc of X,the carrier of V
for g1 being PartFunc of Y,the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let g be PartFunc of X,the carrier of V; :: thesis: for g1 being PartFunc of Y,the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let g1 be PartFunc of Y,the carrier of V; :: thesis: ( g = g1 implies r (#) g1 = r (#) g )
assume AS: g = g1 ; :: thesis: r (#) g1 = r (#) g
P0: dom (r (#) g) = dom g by VFUNCT_1:def 4
.= dom g1 by AS ;
P1: r (#) g is PartFunc of Y,the carrier of V by RELSET_1:13, P0;
for c being Element of Y st c in dom (r (#) g) holds
(r (#) g) /. c = r * (g1 /. c) by VFUNCT_1:def 4, AS;
hence r (#) g1 = r (#) g by P1, P0, VFUNCT_1:def 4; :: thesis: verum