let x, A be set ; :: thesis: for m being Nat st x in m -tuples_on A holds
x is FinSequence of A
let m be Nat; :: thesis: ( x in m -tuples_on A implies x is FinSequence of A )
assume B1: x in m -tuples_on A ; :: thesis: x is FinSequence of A
then reconsider p = x as m -element FinSequence by FINSEQ_2:141;
p in Funcs ((Seg m),A) by B1, Lm21;
then consider f being Function such that
B2: ( p = f & dom f = Seg m & rng f c= A ) by FUNCT_2:def 2;
thus x is FinSequence of A by B2, FINSEQ_1:def 4; :: thesis: verum