let D be non empty set ; :: thesis: for n being Nat
for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds
(f1 ^' f2) /. n = f1 /. n
let n be Nat; :: thesis: for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds
(f1 ^' f2) /. n = f1 /. n
let f1, f2 be FinSequence of D; :: thesis: ( 1 <= n & n <= len f1 implies (f1 ^' f2) /. n = f1 /. n )
assume that
A1: 1 <= n and
A2: n <= len f1 ; :: thesis: (f1 ^' f2) /. n = f1 /. n
per cases ( f2 = {} or f2 <> {} ) ;
suppose f2 = {} ; :: thesis: (f1 ^' f2) /. n = f1 /. n
hence (f1 ^' f2) /. n = f1 /. n by Th55; :: thesis: verum
end;
suppose A3: f2 <> {} ; :: thesis: (f1 ^' f2) /. n = f1 /. n
then A4: (len f1) + 0 < (len f1) + (len f2) by XREAL_1:6;
(len (f1 ^' f2)) + 1 = (len f1) + (len f2) by A3, Th13;
then n < (len (f1 ^' f2)) + 1 by A2, A4, XXREAL_0:2;
then n <= len (f1 ^' f2) by NAT_1:13;
hence (f1 ^' f2) /. n = (f1 ^' f2) . n by A1, FINSEQ_4:15
.= f1 . n by A1, A2, Th14
.= f1 /. n by A1, A2, FINSEQ_4:15 ;
:: thesis: verum
end;
end;