theorem :: ORDINAL4:32

for A, C being Ordinal st 1 in C holds
A c= exp (C,A)