reconsider u = u1, v = v1 as Vector of M by Th48;
let W1, W2 be Element of setvect M; :: thesis: ( ( for u, v being Vector of M st u1 = u & v1 = v holds
W1 = u + v ) & ( for u, v being Vector of M st u1 = u & v1 = v holds
W2 = u + v ) implies W1 = W2 )
assume that
A1: for u, v being Vector of M st u1 = u & v1 = v holds
W1 = u + v and
A2: for u, v being Vector of M st u1 = u & v1 = v holds
W2 = u + v ; :: thesis: W1 = W2
W1 = u + v by A1;
hence W1 = W2 by A2; :: thesis: verum