let f be FinSequence of LTLB_WFF ; :: thesis: for k, n being Nat st n <= k holds
(con f) . n = (con (f | k)) . n
let k, n be Nat; :: thesis: ( n <= k implies (con f) . n = (con (f | k)) . n )
defpred S₁[ Nat] means ( $1 <= k implies (con f) . $1 = (con (f | k)) . $1 );

A1: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume A3: i + 1 <= k ; :: thesis: (con f) . (i + 1) = (con (f | k)) . (i + 1)
then A4: 1 <= k by NAT_1:25;
A5: i < k by A3, NAT_1:13;

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

suppose A6: k <= len f ; :: thesis: (con f) . (i + 1) = (con (f | k)) . (i + 1)

then A7: len (f | k) = k by FINSEQ_1:59;
A8: i < len (f | k) by A5, FINSEQ_1:59, A6;
then A9: i < len (con (f | k)) by Def2;
i + 1 <= len f by A6, A3, XXREAL_0:2;
then A10: i < len f by NAT_1:13;
then A11: i < len (con f) by Def2;

per cases ( i = 0 or 1 <= i ) by NAT_1:25;

suppose A12: i = 0 ; :: thesis: (con f) . (i + 1) = (con (f | k)) . (i + 1)

hence (con f) . (i + 1) = f . 1 by Def2, A6, A3
.= (f | k) . 1 by A4, FINSEQ_3:112
.= (con (f | k)) . (i + 1) by Def2, A12, A7, A3 ;
:: thesis: verum

end;

suppose A13: 1 <= i ; :: thesis: (con f) . (i + 1) = (con (f | k)) . (i + 1)

1 <= i + 1 by XREAL_1:31;
then A14: i + 1 in Seg k by A3;
k in Seg (len f) by A6, A4;
then k in dom f by FINSEQ_1:def 3;
then A15: f /. (i + 1) = (f | k) /. (i + 1) by A14, FINSEQ_4:71;
A16: (con f) /. i = (con f) . i by A11, A13, FINSEQ_4:15
.= (con (f | k)) /. i by A9, A13, FINSEQ_4:15, A2, A3, NAT_1:13 ;
thus (con f) . (i + 1) = ((con f) /. i) '&&' (f /. (i + 1)) by Def2, A10, A13
.= (con (f | k)) . (i + 1) by Def2, A13, A8, A15, A16 ; :: thesis: verum

end;

end;

end;

suppose k > len f ; :: thesis: (con f) . (i + 1) = (con (f | k)) . (i + 1)

hence (con f) . (i + 1) = (con (f | k)) . (i + 1) by FINSEQ_1:58; :: thesis: verum

end;

end;

end;

end;

(con f) . 0 = 0
.= (con (f | k)) . 0 ;
then A17: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A1);
hence ( n <= k implies (con f) . n = (con (f | k)) . n ) ; :: thesis: verum