let X be non empty set ; :: thesis: for x being object st x in X * holds
ex n being Nat st x in n -tuples_on X
let x be object ; :: thesis: ( x in X * implies ex n being Nat st x in n -tuples_on X )
assume x in X * ; :: thesis: ex n being Nat st x in n -tuples_on X
then reconsider x = x as Element of X * ;
reconsider y = x as FinSequence of X ;
take len y ; :: thesis: x in (len y) -tuples_on X
y is Element of (len y) -tuples_on X by FINSEQ_2:92;
hence x in (len y) -tuples_on X ; :: thesis: verum