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