let R be Ring; :: thesis: for n being Nat
for u being Element of (R ^* n)
for v being Element of n -tuples_on the carrier of R
for a being Element of R st u = v holds
a * u = a * v
let n be Nat; :: thesis: for u being Element of (R ^* n)
for v being Element of n -tuples_on the carrier of R
for a being Element of R st u = v holds
a * u = a * v
let u be Element of (R ^* n); :: thesis: for v being Element of n -tuples_on the carrier of R
for a being Element of R st u = v holds
a * u = a * v
let v be Element of n -tuples_on the carrier of R; :: thesis: for a being Element of R st u = v holds
a * u = a * v
let a be Element of R; :: thesis: ( u = v implies a * u = a * v )
assume A: u = v ; :: thesis: a * u = a * v
thus a * u = the lmult of (R ^* n) . (a,u) by VECTSP_1:def 12
.= (vector_mult (n,R)) . (a,v) by A, DEF
.= a * v by Defm ; :: thesis: verum