now :: thesis: for b, c being Ordinal st b in c & c in dom (A | a) holds
(A | a) . b c= (A | a) . c

let b, c be Ordinal; :: thesis: ( b in c & c in dom (A | a) implies (A | a) . b c= (A | a) . c )
assume A1: ( b in c & c in dom (A | a) ) ; :: thesis: (A | a) . b c= (A | a) . c
then A2: ( (A | a) . b = A . b & (A | a) . c = A . c ) by ORDINAL1:10, FUNCT_1:47;
c in dom A by A1, RELAT_1:57;
hence (A | a) . b c= (A | a) . c by A1, A2, ORDINAL5:def 2; :: thesis: verum

end;

hence A | a is non-decreasing by ORDINAL5:def 2; :: thesis: verum