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

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