for U1 being Universal_Algebra
for a being FinSequence of U1 holds (id the carrier of U1) * a = a