let M be MidSp; :: thesis: for u, v being Vector of M ex w being Vector of M 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 )] ~ )
let u, v be Vector of M; :: thesis: ex w being Vector of M 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 )] ~ )
consider p being Element of [:the carrier of M,the carrier of M:] such that
A1: u = p ~ by Def8;
consider q being Element of [:the carrier of M,the carrier of M:] such that
A2: v = q ~ by Def8;
consider d being Element of M such that
A3: q `1 ,q `2 @@ p `2 ,d by Th26;
take [(p `1 ),d] ~ ; :: thesis: ex p, q being Element of [:the carrier of M,the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & [(p `1 ),d] ~ = [(p `1 ),(q `2 )] ~ )
take p9 = p; :: thesis: ex q being Element of [:the carrier of M,the carrier of M:] st
( u = p9 ~ & v = q ~ & p9 `2 = q `1 & [(p `1 ),d] ~ = [(p9 `1 ),(q `2 )] ~ )
take q9 = [(p `2 ),d]; :: thesis: ( u = p9 ~ & v = q9 ~ & p9 `2 = q9 `1 & [(p `1 ),d] ~ = [(p9 `1 ),(q9 `2 )] ~ )
thus u = p9 ~ by A1; :: thesis: ( v = q9 ~ & p9 `2 = q9 `1 & [(p `1 ),d] ~ = [(p9 `1 ),(q9 `2 )] ~ )
( q9 `1 = p `2 & q9 `2 = d ) by MCART_1:7;
then q ## q9 by A3, Def6;
hence v = q9 ~ by A2, Th42; :: thesis: ( p9 `2 = q9 `1 & [(p `1 ),d] ~ = [(p9 `1 ),(q9 `2 )] ~ )
thus p9 `2 = q9 `1 by MCART_1:7; :: thesis: [(p `1 ),d] ~ = [(p9 `1 ),(q9 `2 )] ~
thus [(p `1 ),d] ~ = [(p9 `1 ),(q9 `2 )] ~ by MCART_1:7; :: thesis: verum