let i be Nat; :: thesis: for x, A being set st x in i -tuples_on A holds
x is i -element FinSequence
let x, A be set ; :: thesis: ( x in i -tuples_on A implies x is i -element FinSequence )
assume x in i -tuples_on A ; :: thesis: x is i -element 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 -element FinSequence by CARD_1:def 7; :: thesis: verum