let f be FinSequence; :: thesis: for n being Nat holds (f | n) ^ (f /^ n) = f
let n be Nat; :: thesis: (f | n) ^ (f /^ n) = f
reconsider D = (rng f) \/ {1} as non empty set ;
f is FinSequence of D by FINSEQ_1:def 4, XBOOLE_1:7;
hence (f | n) ^ (f /^ n) = f by Th8A; :: thesis: verum