for j1 being Integer holds j1 = (@' 1) |^ j1