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

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