theorem Th9: :: CALCUL_1:9

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