let D be non empty set ; for f1, f2 being FinSequence of D
for n being Nat st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
let f1, f2 be FinSequence of D; for n being Nat st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
let n be Nat; ( 1 <= n & n <= len f2 implies (f1 ^ f2) /. (n + (len f1)) = f2 /. n )
assume that
A1:
1 <= n
and
A2:
n <= len f2
; (f1 ^ f2) /. (n + (len f1)) = f2 /. n
A3:
len f1 < n + (len f1)
by A1, NAT_1:19;
len (f1 ^ f2) = (len f1) + (len f2)
by FINSEQ_1:22;
then A4:
n + (len f1) <= len (f1 ^ f2)
by A2, XREAL_1:6;
n + (len f1) >= n
by NAT_1:11;
then
n + (len f1) >= 1
by A1, XXREAL_0:2;
hence (f1 ^ f2) /. (n + (len f1)) =
(f1 ^ f2) . (n + (len f1))
by A4, FINSEQ_4:15
.=
f2 . ((n + (len f1)) - (len f1))
by A3, A4, FINSEQ_1:24
.=
f2 /. n
by A1, A2, FINSEQ_4:15
;
verum