for A being Ordinal holds
( 1 *^ A = A & A *^ 1 = A )