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

per cases ( j = 0 or j <> 0 ) ;

suppose A3: j = 0 ; :: thesis: (maxPrefix p,q) . j = p . j

then A4: not j in dom p by FINSEQ_3:26;
not j in dom (maxPrefix p,q) by A3, FINSEQ_3:26;
hence (maxPrefix p,q) . j = 0 by FUNCT_1:def 4
.= p . j by A4, FUNCT_1:def 4 ;
:: thesis: verum

end;

suppose j <> 0 ; :: thesis: (maxPrefix p,q) . j = p . j

then 0 + 1 <= j by NAT_1:13;
then j in dom (maxPrefix p,q) by A1, FINSEQ_3:27;
hence (maxPrefix p,q) . j = p . j by A2, GRFUNC_1:8; :: thesis: verum

end;

end;