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