let m, n be Nat; :: thesis: ( m in dom q1 & n in dom (Shift (q2,(len p1))) implies m < n )
assume that
A5: m in dom q1 and
A6: n in dom (Shift (q2,(len p1))) ; :: thesis: m < n
A7: dom p1 = Seg (len p1) by FINSEQ_1:def 3
.= { k where k is Nat : ( 1 <= k & k <= len p1 ) } ;
A8: dom (Shift (p2,(len p1))) = { k where k is Nat : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) } by Th39;
A9: dom q1 c= dom p1 by A1, GRFUNC_1:2;
A10: dom (Shift (q2,(len p1))) c= dom (Shift (p2,(len p1))) by A2, Lm7;
A11: m in dom p1 by A5, A9;
A12: n in dom (Shift (p2,(len p1))) by A6, A10;
consider k3 being Nat such that
A13: k3 = m and
1 <= k3 and
A14: k3 <= len p1 by A7, A11;
consider k4 being Nat such that
A15: k4 = n and
A16: (len p1) + 1 <= k4 and
k4 <= (len p1) + (len p2) by A8, A12;
len p1 < (len p1) + 1 by XREAL_1:29;
then k3 <= (len p1) + 1 by A14, XXREAL_0:2;
then A17: k3 <= k4 by A16, XXREAL_0:2;
k3 <> k4 by A5, A6, A9, A13, A15, Th47, XBOOLE_0:3;
hence m < n by A13, A15, A17, XXREAL_0:1; :: thesis: verum