let n be Nat; :: thesis: for f being Permutation of (Seg n) holds f is FinSequence of Seg n
let f be Permutation of (Seg n); :: thesis: f is FinSequence of Seg n
A1: rng f c= Seg n by RELAT_1:def 19;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f is FinSequence of Seg n

hence f is FinSequence of Seg n by A1, FINSEQ_1:def 4; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: f is FinSequence of Seg n

then dom f = Seg n by FUNCT_2:def 1;
then f is FinSequence by FINSEQ_1:def 2;
hence f is FinSequence of Seg n by A1, FINSEQ_1:def 4; :: thesis: verum

end;

end;