let p, q be FinSequence; :: thesis: ( not p is_a_prefix_of q & not q is_a_prefix_of p implies p . ((len (maxPrefix p,q)) + 1) <> q . ((len (maxPrefix p,q)) + 1) )
assume that
A1: not p c= q and
A2: not q c= p and
A3: p . ((len (maxPrefix p,q)) + 1) = q . ((len (maxPrefix p,q)) + 1) ; :: thesis: contradiction
set dI = len (maxPrefix p,q);
set mP = maxPrefix p,q;
set lmP = (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>;

A4: now

let x be set ; :: thesis: ( x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) implies ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁ )
assume A5: x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁
reconsider n = x as Nat by A5;
A6: 1 <= n by A5, FINSEQ_3:27;
n <= len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) by A5, FINSEQ_3:27;
then A7: n <= (len (maxPrefix p,q)) + 1 by FINSEQ_2:19;

per cases ( n <= len (maxPrefix p,q) or n = (len (maxPrefix p,q)) + 1 ) by A7, NAT_1:8;

suppose A8: n <= len (maxPrefix p,q) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁

then n in dom (maxPrefix p,q) by A6, FINSEQ_3:27;
hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = (maxPrefix p,q) . x by FINSEQ_1:def 7
.= q . x by A8, Th6 ;
:: thesis: verum

end;

suppose n = (len (maxPrefix p,q)) + 1 ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁

hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = q . x by A3, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

A9: now

let x be set ; :: thesis: ( x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) implies ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁ )
assume A10: x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁
reconsider n = x as Nat by A10;
A11: 1 <= n by A10, FINSEQ_3:27;
n <= len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) by A10, FINSEQ_3:27;
then A12: n <= (len (maxPrefix p,q)) + 1 by FINSEQ_2:19;

per cases ( n <= len (maxPrefix p,q) or n = (len (maxPrefix p,q)) + 1 ) by A12, NAT_1:8;

suppose A13: n <= len (maxPrefix p,q) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁

then n in dom (maxPrefix p,q) by A11, FINSEQ_3:27;
hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = (maxPrefix p,q) . x by FINSEQ_1:def 7
.= p . x by A13, Th6 ;
:: thesis: verum

end;

suppose n = (len (maxPrefix p,q)) + 1 ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁

hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = p . x by FINSEQ_1:59; :: thesis: verum

end;

end;

end;

A14: len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) = (len (maxPrefix p,q)) + 1 by FINSEQ_2:19;
len (maxPrefix p,q) < len q by A2, Th8;
then len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) <= len q by A14, NAT_1:13;
then dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) c= dom q by FINSEQ_3:32;
then A15: (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*> c= q by A4, GRFUNC_1:8;
len (maxPrefix p,q) < len p by A1, Th8;
then len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) <= len p by A14, NAT_1:13;
then dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) c= dom p by FINSEQ_3:32;
then (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*> c= p by A9, GRFUNC_1:8;
then (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*> c= maxPrefix p,q by A15, Def1;
then len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) <= len (maxPrefix p,q) by FINSEQ_1:84;
then (len (maxPrefix p,q)) + 1 <= len (maxPrefix p,q) by FINSEQ_2:19;
hence contradiction by NAT_1:13; :: thesis: verum