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 Th34;

u = vect (a,b) by A1;

hence ex b being Element of M st u = vect (a,b) ; :: thesis: verum

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 Th34;

u = vect (a,b) by A1;

hence ex b being Element of M st u = vect (a,b) ; :: thesis: verum