theorem :: WALLIS01:18

RAlgebra REAL is RealLinearSpace ;