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

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