consider p being Element of [: the carrier of M, the carrier of M:] such that
A1: u = p ~ by Def7;
consider q being Element of [: the carrier of M, the carrier of M:] such that
A2: v = q ~ by Def7;
consider d being Element of M such that
A3: q `1 ,q `2 @@ p `2 ,d by Th15;
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)] ~ )
q ## q9 by A3;
hence v = q9 ~ by A2, Th27; :: thesis: ( p9 `2 = q9 `1 & [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~ )
thus p9 `2 = q9 `1 ; :: thesis: [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~
thus [(p `1),d] ~ = [(p9 `1),(q9 `2)] ~ ; :: thesis: verum