let M be MidSp; :: thesis: for u, v, w, w9 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w9 = [(p `1),(q `2)] ~ ) holds
w = w9
let u, v, w, w9 be Vector of M; :: thesis: ( ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w9 = [(p `1),(q `2)] ~ ) implies w = w9 )
given p, q being Element of [: the carrier of M, the carrier of M:] such that A1: u = p ~ and
A2: v = q ~ and
A3: p `2 = q `1 and
A4: w = [(p `1),(q `2)] ~ ; :: thesis: ( for p, q being Element of [: the carrier of M, the carrier of M:] holds
( not u = p ~ or not v = q ~ or not p `2 = q `1 or not w9 = [(p `1),(q `2)] ~ ) or w = w9 )
given p9, q9 being Element of [: the carrier of M, the carrier of M:] such that A5: u = p9 ~ and
A6: v = q9 ~ and
A7: p9 `2 = q9 `1 and
A8: w9 = [(p9 `1),(q9 `2)] ~ ; :: thesis: w = w9
q ## q9 by A2, A6, Th28;
then A9: q `1 ,q `2 @@ q9 `1 ,q9 `2 ;
p ## p9 by A1, A5, Th28;
then p `1 ,p `2 @@ p9 `1 ,p9 `2 ;
then p `1 ,q `2 @@ p9 `1 ,q9 `2 by A3, A7, A9, Th18;
hence w = w9 by A4, A8, Th19, Th27; :: thesis: verum