for A being Ordinal holds A +^ 0 = A