let f be FinSequence; :: thesis: for a, b being Nat holds (f /^ a) /^ b = f /^ (a + b)
let a, b be Nat; :: thesis: (f /^ a) /^ b = f /^ (a + b)
ex D being non empty set st f is FinSequence of D by Th0;
hence (f /^ a) /^ b = f /^ (a + b) by FINSEQ_6:81; :: thesis: verum