let Y be set ; :: thesis: for m being Nat
for p being FinSequence st p is Y -valued & p is m -element holds
p in m -tuples_on Y
let m be Nat; :: thesis: for p being FinSequence st p is Y -valued & p is m -element holds
p in m -tuples_on Y
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let p be FinSequence; :: thesis: ( p is Y -valued & p is m -element implies p in m -tuples_on Y )
assume ( p is Y -valued & p is m -element ) ; :: thesis: p in m -tuples_on Y
then ( rng p c= Y & len p = mm ) by CARD_1:def 7;
hence p in m -tuples_on Y by FINSEQ_2:132; :: thesis: verum