let n be Nat; :: thesis: for x being VECTOR of (REAL-NS n)

for y being Element of REAL n

for a being Real 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 st x = y holds

a * x = a * y

let y be Element of REAL n; :: thesis: for a being Real st x = y holds

a * x = a * y

let a be Real; :: thesis: ( x = y implies a * x = a * y )

assume A1: x = y ; :: thesis: a * x = a * y

reconsider a = a as Real ;

a * x = (Euclid_mult n) . (a,x) by Def4

.= a * y by A1, Def2 ;

hence a * x = a * y ; :: thesis: verum

for y being Element of REAL n

for a being Real 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 st x = y holds

a * x = a * y

let y be Element of REAL n; :: thesis: for a being Real st x = y holds

a * x = a * y

let a be Real; :: thesis: ( x = y implies a * x = a * y )

assume A1: x = y ; :: thesis: a * x = a * y

reconsider a = a as Real ;

a * x = (Euclid_mult n) . (a,x) by Def4

.= a * y by A1, Def2 ;

hence a * x = a * y ; :: thesis: verum