now :: thesis: for a, b being Ordinal st a in b & b in dom (omega -exponent A) holds
(omega -exponent A) . b in (omega -exponent A) . a

let a, b be Ordinal; :: thesis: ( a in b & b in dom (omega -exponent A) implies (omega -exponent A) . b in (omega -exponent A) . a )
assume A1: ( a in b & b in dom (omega -exponent A) ) ; :: thesis: (omega -exponent A) . b in (omega -exponent A) . a
then A2: b in dom A by Def1;
then ( (omega -exponent A) . a = omega -exponent (A . a) & (omega -exponent A) . b = omega -exponent (A . b) ) by A1, Def1, ORDINAL1:10;
hence (omega -exponent A) . b in (omega -exponent A) . a by A1, A2, ORDINAL5:def 11; :: thesis: verum

end;

hence omega -exponent A is decreasing by ORDINAL5:def 1; :: thesis: verum