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

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

given a being Ordinal 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;
hence b c= c by A2; :: according to XBOOLE_0:def 10 :: thesis: c c= b
b in dom f by A1, A2;
hence c c= b by A2; :: thesis: verum

end;

end;

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