let i be Nat; :: thesis: for x, A being set st x in i -tuples_on A holds
x is i -long FinSequence
let x, A be set ; :: thesis: ( x in i -tuples_on A implies x is i -long FinSequence )
assume x in i -tuples_on A ; :: thesis: x is i -long FinSequence
then x in { s where s is Element of A * : len s = i } ;
then ex s being Element of A * st
( x = s & len s = i ) ;
hence x is i -long FinSequence by FINSEQ_1:def 18; :: thesis: verum