reconsider u2 = u1, v2 = v1 as Vector of M by Th48;
reconsider suma = u2 + v2 as Element of setvect M by Th48;
take suma ; :: thesis: for u, v being Vector of M st u1 = u & v1 = v holds
suma = u + v
thus for u, v being Vector of M st u1 = u & v1 = v holds
suma = u + v ; :: thesis: verum