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

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