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;

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 )
;

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;then f is FinSequence by FINSEQ_1:def 2;

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