let R be Ring; :: thesis: for n being Nat
for u, v being Element of (R ^* n)
for a, b being Element of n -tuples_on the carrier of R st u = a & v = b holds
a + b = u + v
let n be Nat; :: thesis: for u, v being Element of (R ^* n)
for a, b being Element of n -tuples_on the carrier of R st u = a & v = b holds
a + b = u + v
let u, v be Element of (R ^* n); :: thesis: for a, b being Element of n -tuples_on the carrier of R st u = a & v = b holds
a + b = u + v
let a, b be Element of n -tuples_on the carrier of R; :: thesis: ( u = a & v = b implies a + b = u + v )
assume A: ( u = a & v = b ) ; :: thesis: a + b = u + v
thus u + v = (vector_add (n,R)) . (a,b) by A, DEF
.= a + b by Defa ; :: thesis: verum