let n be Nat; :: thesis: for f being Function st dom f = NAT holds
f | (Seg n) is FinSequence
let f be Function; :: thesis: ( dom f = NAT implies f | (Seg n) is FinSequence )
assume dom f = NAT ; :: thesis: f | (Seg n) is FinSequence
then dom (f | (Seg n)) = Seg n by RELAT_1:62;
hence f | (Seg n) is FinSequence by FINSEQ_1:def 2; :: thesis: verum