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

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