let L be non empty addLoopStr ; :: thesis: for x being FinSequence of L holds x is Element of (len x) -tuples_on the carrier of L
let x be FinSequence of L; :: thesis: x is Element of (len x) -tuples_on the carrier of L
x is Element of the carrier of L * by FINSEQ_1:def 11;
then x in { s where s is Element of the carrier of L * : len s = len x } ;
hence x is Element of (len x) -tuples_on the carrier of L by FINSEQ_2:def 4; :: thesis: verum