let p be FinSequence; :: thesis: for f being Function st dom f = dom p holds
f is FinSequence
dom p = Seg (len p) by FINSEQ_1:def 3;
hence for f being Function st dom f = dom p holds
f is FinSequence by FINSEQ_1:def 2; :: thesis: verum