theorem Th16: :: GR_CY_1:16

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