let D be non empty set ; :: thesis: for n being Nat
for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds
(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)
let n be Nat; :: thesis: for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds
(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)
let f1, f2 be FinSequence of D; :: thesis: ( 1 <= n & n < len f2 implies (f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1) )
assume that
A1: 1 <= n and
A2: n < len f2 ; :: thesis: (f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)
A3: n + 1 <= len f2 by A2, NAT_1:13;

A4: now :: thesis: (len f1) + n <= len (f1 ^' f2)

per cases ( f2 <> {} or f2 = {} ) ;

suppose A5: f2 <> {} ; :: thesis: (len f1) + n <= len (f1 ^' f2)

A6: (len f1) + n < (len f1) + (len f2) by A2, XREAL_1:6;
(len (f1 ^' f2)) + 1 = (len f1) + (len f2) by A5, Th13;
hence (len f1) + n <= len (f1 ^' f2) by A6, NAT_1:13; :: thesis: verum

end;

suppose f2 = {} ; :: thesis: (len f1) + n <= len (f1 ^' f2)

hence (len f1) + n <= len (f1 ^' f2) by A2; :: thesis: verum

end;

end;

end;

A7: 0 + 1 <= n + 1 by XREAL_1:6;
0 + 1 <= (len f1) + n by A1, XREAL_1:7;
hence (f1 ^' f2) /. ((len f1) + n) = (f1 ^' f2) . ((len f1) + n) by A4, FINSEQ_4:15
.= f2 . (n + 1) by A1, A2, Th15
.= f2 /. (n + 1) by A7, A3, FINSEQ_4:15 ;
:: thesis: verum