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