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