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 A1: g = g1 ; :: thesis: r (#) g1 = r (#) g
A2: dom (r (#) g) = dom g by VFUNCT_1:def 4
.= dom g1 by A1 ;
A3: r (#) g is PartFunc of Y, the carrier of V by ;
for c being Element of Y st c in dom (r (#) g) holds
(r (#) g) /. c = r * (g1 /. c) by ;
hence r (#) g1 = r (#) g by ; :: thesis: verum