let D be non empty set ; :: thesis: for f1, f2 being FinSequence of D
for n being Element of NAT st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
let f1, f2 be FinSequence of D; :: thesis: for n being Element of NAT st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len f2 implies (f1 ^ f2) /. (n + (len f1)) = f2 /. n )
assume that
A1: 1 <= n and
A2: n <= len f2 ; :: thesis: (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 ;
:: thesis: verum