:: deftheorem defines R_Algebra_of_Real-Valued-Random-Variables RANDOM_2:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega holds R_Algebra_of_Real-Valued-Random-Variables Sigma = AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);