set f = <%a%>;
A1: ( dom <%a%> = 1 & <%a%> . 0 = a ) by AFINSQ_1:def 4;
hence for c, b being Ordinal st c in b & b in dom <%a%> holds
<%a%> . b in <%a%> . c by ORDINAL3:15, TARSKI:def 1; :: according to ORDINAL5:def 1 :: thesis: <%a%> is increasing
let c be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not c in b₁ or not b₁ in dom <%a%> or <%a%> . c in <%a%> . b₁ )
let b be Ordinal; :: thesis: ( not c in b or not b in dom <%a%> or <%a%> . c in <%a%> . b )
thus ( not c in b or not b in dom <%a%> or <%a%> . c in <%a%> . b ) by A1, ORDINAL3:15, TARSKI:def 1; :: thesis: verum