let A, x 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 A1: 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 A1, Lm7;
then consider f being Function such that
A2: ( p = f & dom f = Seg m & rng f c= A ) by FUNCT_2:def 2;
thus x is FinSequence of A by A2, FINSEQ_1:def 4; :: thesis: verum