let M be MidSp; :: thesis: for u, v, w, w' 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 & w' = [(p `1 ),(q `2 )] ~ ) holds
w = w'
let u, v, w, w' 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 & w' = [(p `1 ),(q `2 )] ~ ) implies w = w' )
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 w' = [(p `1 ),(q `2 )] ~ ) or w = w' )
given p', q' being Element of [:the carrier of M,the carrier of M:] such that A5: u = p' ~ and
A6: v = q' ~ and
A7: p' `2 = q' `1 and
A8: w' = [(p' `1 ),(q' `2 )] ~ ; :: thesis: w = w'
p ## p' by A1, A5, Th43;
then A9: p `1 ,p `2 @@ p' `1 ,p' `2 by Def6;
q ## q' by A2, A6, Th43;
then q `1 ,q `2 @@ q' `1 ,q' `2 by Def6;
then p `1 ,q `2 @@ p' `1 ,q' `2 by A3, A7, A9, Th29;
hence w = w' by A4, A8, Th31, Th42; :: thesis: verum