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 A1: x in { s where s is Element of the carrier of L * : len s = len x } ;
thus x is Element of (len x) -tuples_on the carrier of L by A1, FINSEQ_2:def 4; :: thesis: verum