let n be Element of NAT ; :: thesis: for x being VECTOR of (REAL-NS n)
for y being Element of REAL n
for a being real number st x = y holds
a * x = a * y
let x be Point of (REAL-NS n); :: thesis: for y being Element of REAL n
for a being real number st x = y holds
a * x = a * y
let y be Element of REAL n; :: thesis: for a being real number st x = y holds
a * x = a * y
let a be real number ; :: thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; :: thesis: a * x = a * y
reconsider a = a as Real by XREAL_0:def 1;
a * x = (Euclid_mult n) . a,x by Def4
.= a * y by A1, Def2 ;
hence a * x = a * y ; :: thesis: verum