consider n being Nat such that
A1: A, Seg n are_equipotent by Th56;
consider f being Function such that
A2: f is one-to-one and
A3: dom f = Seg n and
A4: rng f = A by A1, WELLORD2:def 4;
f is FinSequence by A3, Def2;
then reconsider f = f as FinSequence of A by A4, Def4;
take f ; :: thesis: ( f is onto & f is one-to-one )
thus ( f is onto & f is one-to-one ) by A2, A4, FUNCT_2:def 3; :: thesis: verum