let D be non empty set ; :: thesis: for f1 being FinSequence of D
for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)
let f1 be FinSequence of D; :: thesis: for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)
let f2 be non trivial FinSequence of D; :: thesis: (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)
A1: (len (f1 ^' f2)) + 1 = (len f1) + (len f2) by Th13;
2 <= len f2 by NAT_D:60;
then A2: 1 < len f2 by XXREAL_0:2;
then 1 + 0 < (len f1) + (len f2) by XREAL_1:8;
then 1 <= len (f1 ^' f2) by A1, NAT_1:13;
hence (f1 ^' f2) /. (len (f1 ^' f2)) = (f1 ^' f2) . (len (f1 ^' f2)) by FINSEQ_4:15
.= f2 . (len f2) by A2, Th16
.= f2 /. (len f2) by A2, FINSEQ_4:15 ;
:: thesis: verum