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

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

end;

hence A | a is increasing by ORDINAL2:def 12; :: thesis: verum