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 13;
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 RELAT_1:def 19, CARD_1:def 13;
hence p in m -tuples_on Y by FINSEQ_2:152; :: thesis: verum