let D be non empty set ; 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; 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; ( 1 <= n & n < len f2 implies (f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1) )
assume that
A1:
1 <= n
and
A2:
n < len f2
; (f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)
A3:
n + 1 <= len f2
by A2, NAT_1:13;
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
;
verum