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 = [a,b] ~

let a be Element of M; :: thesis: for u being Vector of M ex b being Element of M st u = [a,b] ~

let u be Vector of M; :: thesis: ex b being Element of M st u = [a,b] ~

consider p being Element of [: the carrier of M, the carrier of M:] such that

A1: u = p ~ by Def7;

consider b being Element of M such that

A2: p `1 ,p `2 @@ a,b by Th15;

[(p `1),(p `2)] ## [a,b] by A2;

then p ## [a,b] ;

then p ~ = [a,b] ~ by Th27;

hence ex b being Element of M st u = [a,b] ~ by A1; :: thesis: verum

for u being Vector of M ex b being Element of M st u = [a,b] ~

let a be Element of M; :: thesis: for u being Vector of M ex b being Element of M st u = [a,b] ~

let u be Vector of M; :: thesis: ex b being Element of M st u = [a,b] ~

consider p being Element of [: the carrier of M, the carrier of M:] such that

A1: u = p ~ by Def7;

consider b being Element of M such that

A2: p `1 ,p `2 @@ a,b by Th15;

[(p `1),(p `2)] ## [a,b] by A2;

then p ## [a,b] ;

then p ~ = [a,b] ~ by Th27;

hence ex b being Element of M st u = [a,b] ~ by A1; :: thesis: verum