let M be MidSp; 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; for u being Vector of M ex b being Element of M st u = [a,b] ~
let u be Vector of M; 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; verum