the carrier of L c= the carrier of L ;
then reconsider u1 = u, v1 = v as Element of n -tuples_on the carrier of L by FINSEQ_2:109;
u1 + v1 is Element of n -tuples_on the carrier of L ;
hence u + v is n -element ; :: thesis: verum