let A be set ; :: thesis: for i being Element of NAT
for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
let i be Element of NAT ; :: thesis: for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
let p be FinSequence of A; :: thesis: ( p in i -tuples_on A iff len p = i )
rng p c= A by RELAT_1:def 19;
hence ( p in i -tuples_on A iff len p = i ) by Th130; :: thesis: verum