set S = the RealLinearSpace;

take <* the RealLinearSpace*> ; :: thesis: ( not <* the RealLinearSpace*> is empty & <* the RealLinearSpace*> is RealLinearSpace-yielding )

thus not <* the RealLinearSpace*> is empty ; :: thesis: <* the RealLinearSpace*> is RealLinearSpace-yielding

let x be set ; :: according to PRVECT_2:def 3 :: thesis: ( x in rng <* the RealLinearSpace*> implies x is RealLinearSpace )

assume that

A1: x in rng <* the RealLinearSpace*> and

A2: x is not RealLinearSpace ; :: thesis: contradiction

x in { the RealLinearSpace} by A1, FINSEQ_1:38;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

take <* the RealLinearSpace*> ; :: thesis: ( not <* the RealLinearSpace*> is empty & <* the RealLinearSpace*> is RealLinearSpace-yielding )

thus not <* the RealLinearSpace*> is empty ; :: thesis: <* the RealLinearSpace*> is RealLinearSpace-yielding

let x be set ; :: according to PRVECT_2:def 3 :: thesis: ( x in rng <* the RealLinearSpace*> implies x is RealLinearSpace )

assume that

A1: x in rng <* the RealLinearSpace*> and

A2: x is not RealLinearSpace ; :: thesis: contradiction

x in { the RealLinearSpace} by A1, FINSEQ_1:38;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum