let p, q be FinSequence; :: thesis: for j being Nat st j <= len (maxPrefix (p,q)) holds
p . j = q . j
let j be Nat; :: thesis: ( j <= len (maxPrefix (p,q)) implies p . j = q . j )
assume A1: j <= len (maxPrefix (p,q)) ; :: thesis: p . j = q . j
thus p . j = (maxPrefix (p,q)) . j by A1, Th6
.= q . j by A1, Th6 ; :: thesis: verum