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

( 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