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:24;
not j in dom (maxPrefix (p,q)) by A3, FINSEQ_3:24;
hence (maxPrefix (p,q)) . j = 0 by FUNCT_1:def 2
.= p . j by A4, FUNCT_1:def 2 ;
:: 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:25;
hence (maxPrefix (p,q)) . j = p . j by A2, GRFUNC_1:2; :: thesis: verum

end;

end;