let b, c be ordinal number ; :: thesis: ( ( ex a being ordinal number st a in dom f & f is b -based & f is c -based 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 A1: a in dom f ; :: thesis: ( f is b -based & f is c -based implies b = c )
assume A2: ( f is b -based & f is c -based ) ; :: thesis: b = c
thus b = c :: thesis: verum

proof

c in dom f by A1, A2, AB;
hence b c= c by A2, AB; :: according to XBOOLE_0:def 10 :: thesis: c c= b
b in dom f by A1, A2, AB;
hence c c= b by A2, AB; :: thesis: verum

end;

end;

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