set f = <*r*>;
let x be object ; :: according to VALUED_0:def 10 :: thesis: ( not x in dom <*r*> or <*r*> . x is rational )
assume A1: x in dom <*r*> ; :: thesis: <*r*> . x is rational
dom <*r*> = {1} by Def8, Th2;
then x = 1 by A1, TARSKI:def 1;
hence <*r*> . x is rational ; :: thesis: verum