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