theorem :: FSM_3:2

for a, b being FinSequence st ( a ^ b = a or b ^ a = a ) holds
b = {}