let b, c be ordinal number ; :: thesis: ( ( ex a being ordinal number st a in dom f & f is b -limited & f is c -limited implies b = c ) & ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) )

hereby :: thesis: ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c )

given a being ordinal number such that a in dom f ; :: thesis: ( f is b -limited & f is c -limited implies b = c )
assume A2: ( f is b -limited & f is c -limited ) ; :: thesis: b = c
thus b = sup (dom f) by A2, LI
.= c by A2, LI ; :: thesis: verum

end;

thus ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ; :: thesis: verum