set A = the RealNormSpace;
take <* the RealNormSpace*> ; :: thesis: ( not <* the RealNormSpace*> is empty & <* the RealNormSpace*> is RealNormSpace-yielding )
thus not <* the RealNormSpace*> is empty ; :: thesis: <* the RealNormSpace*> is RealNormSpace-yielding
let x be set ; :: according to PRVECT_2:def 10 :: thesis: ( x in rng <* the RealNormSpace*> implies x is RealNormSpace )
assume that
A1: x in rng <* the RealNormSpace*> and
A2: x is not RealNormSpace ; :: thesis: contradiction
x in { the RealNormSpace} by A1, FINSEQ_1:38;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum