for b, c being object
for fin being FinSequence holds 1 < len ((fin ^ <*b*>) ^ <*c*>)