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