let i be natural Number ; :: thesis: for A being set
for x being object st x in i -tuples_on A holds
x is i -element FinSequence
let A be set ; :: thesis: for x being object st x in i -tuples_on A holds
x is i -element FinSequence
let x be object ; :: 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