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