let M be MidSp; :: thesis: for a being Element of M
for u being Vector of M ex b being Element of M st u = vect a,b
let a be Element of M; :: thesis: for u being Vector of M ex b being Element of M st u = vect a,b
let u be Vector of M; :: thesis: ex b being Element of M st u = vect a,b
consider b being Element of M such that
A1: u = [a,b] ~ by Th53;
u = vect a,b by A1;
hence ex b being Element of M st u = vect a,b ; :: thesis: verum