let A be set ; :: thesis: for i being Nat
for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
let i be Nat; :: thesis: for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
let p be FinSequence; :: thesis: ( p in i -tuples_on A iff ( len p = i & rng p c= A ) )

hereby :: thesis: ( len p = i & rng p c= A implies p in i -tuples_on A )

assume p in i -tuples_on A ; :: thesis: ( len p = i & rng p c= A )
then ex q being Element of A * st
( p = q & len q = i ) ;
hence ( len p = i & rng p c= A ) by FINSEQ_1:def 4; :: thesis: verum

end;

assume A1: len p = i ; :: thesis: ( not rng p c= A or p in i -tuples_on A )
assume rng p c= A ; :: thesis: p in i -tuples_on A
then p is FinSequence of A by FINSEQ_1:def 4;
then p in A * by FINSEQ_1:def 11;
hence p in i -tuples_on A by A1; :: thesis: verum