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 p' = p; :: thesis: ex 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 q' = [(p `2 ),d]; :: thesis: ( u = p' ~ & v = q' ~ & p' `2 = q' `1 & [(p `1 ),d] ~ = [(p' `1 ),(q' `2 )] ~ )
thus u = p' ~ by A1; :: thesis: ( v = q' ~ & p' `2 = q' `1 & [(p `1 ),d] ~ = [(p' `1 ),(q' `2 )] ~ )
( q' `1 = p `2 & q' `2 = d ) by MCART_1:7;
then q ## q' by A3, Def6;
hence v = q' ~ by A2, Th42; :: thesis: ( p' `2 = q' `1 & [(p `1 ),d] ~ = [(p' `1 ),(q' `2 )] ~ )
thus p' `2 = q' `1 by MCART_1:7; :: thesis: [(p `1 ),d] ~ = [(p' `1 ),(q' `2 )] ~
thus [(p `1 ),d] ~ = [(p' `1 ),(q' `2 )] ~ by MCART_1:7; :: thesis: verum