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