let f be FinSequence of LTLB_WFF ; :: thesis: for k, n being Nat st n <= k & 1 <= n & n <= len f holds
(con f) /. n = (con (f | k)) /. n
let k, n be Nat; :: thesis: ( n <= k & 1 <= n & n <= len f implies (con f) /. n = (con (f | k)) /. n )
assume that
A1: n <= k and
A2: 1 <= n and
A3: n <= len f ; :: thesis: (con f) /. n = (con (f | k)) /. n
A4: n <= len (con f) by A2, A3, Def2;

per cases ( k <= len f or k > len f ) ;

suppose k <= len f ; :: thesis: (con f) /. n = (con (f | k)) /. n

then A5: n <= len (f | k) by FINSEQ_1:59, A1;
then A6: len (con (f | k)) = len (f | k) by A2, Def2;
thus (con f) /. n = (con f) . n by FINSEQ_4:15, A2, A4
.= (con (f | k)) . n by Th12, A1
.= (con (f | k)) /. n by FINSEQ_4:15, A2, A6, A5 ; :: thesis: verum

end;

suppose k > len f ; :: thesis: (con f) /. n = (con (f | k)) /. n

hence (con f) /. n = (con (f | k)) /. n by FINSEQ_1:58; :: thesis: verum

end;

end;