let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega holds
( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed )
let Sigma be SigmaField of Omega; :: thesis: ( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed )
set W = Real-Valued-Random-Variables-Set Sigma;
set V = RAlgebra Omega;
A1: for v, u being Element of (RAlgebra Omega) st v in Real-Valued-Random-Variables-Set Sigma & u in Real-Valued-Random-Variables-Set Sigma holds
v * u in Real-Valued-Random-Variables-Set Sigma

proof

let v, u be Element of (RAlgebra Omega); :: thesis: ( v in Real-Valued-Random-Variables-Set Sigma & u in Real-Valued-Random-Variables-Set Sigma implies v * u in Real-Valued-Random-Variables-Set Sigma )
assume that
A2: v in Real-Valued-Random-Variables-Set Sigma and
A3: u in Real-Valued-Random-Variables-Set Sigma ; :: thesis: v * u in Real-Valued-Random-Variables-Set Sigma
consider u1 being Real-Valued-Random-Variable of Sigma such that
A4: u1 = u by A3;
reconsider h = v * u as Element of Funcs (Omega,REAL) ;
consider v1 being Real-Valued-Random-Variable of Sigma such that
A5: v1 = v by A2;
(dom v1) /\ (dom u1) = Omega /\ (dom u1) by FUNCT_2:def 1;
then A6: ( ex f being Function st
( h = f & dom f = Omega & rng f c= REAL ) & (dom v1) /\ (dom u1) = Omega /\ Omega ) by FUNCT_2:def 1, FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A5, A4, FUNCSDOM:2;
then v * u = v1 (#) u1 by A6, VALUED_1:def 4;
hence v * u in Real-Valued-Random-Variables-Set Sigma ; :: thesis: verum

end;

for v, u being Element of (RAlgebra Omega) st v in Real-Valued-Random-Variables-Set Sigma & u in Real-Valued-Random-Variables-Set Sigma holds
v + u in Real-Valued-Random-Variables-Set Sigma

proof

let v, u be Element of (RAlgebra Omega); :: thesis: ( v in Real-Valued-Random-Variables-Set Sigma & u in Real-Valued-Random-Variables-Set Sigma implies v + u in Real-Valued-Random-Variables-Set Sigma )
assume that
A7: v in Real-Valued-Random-Variables-Set Sigma and
A8: u in Real-Valued-Random-Variables-Set Sigma ; :: thesis: v + u in Real-Valued-Random-Variables-Set Sigma
consider u1 being Real-Valued-Random-Variable of Sigma such that
A9: u1 = u by A8;
reconsider h = v + u as Element of Funcs (Omega,REAL) ;
consider v1 being Real-Valued-Random-Variable of Sigma such that
A10: v1 = v by A7;
(dom v1) /\ (dom u1) = Omega /\ (dom u1) by FUNCT_2:def 1;
then A11: ( ex f being Function st
( h = f & dom f = Omega & rng f c= REAL ) & (dom v1) /\ (dom u1) = Omega /\ Omega ) by FUNCT_2:def 1, FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A10, A9, FUNCSDOM:1;
then v + u = v1 + u1 by A11, VALUED_1:def 1;
hence v + u in Real-Valued-Random-Variables-Set Sigma ; :: thesis: verum

end;

then A12: Real-Valued-Random-Variables-Set Sigma is add-closed by IDEAL_1:def 1;
A13: RAlgebra Omega is RealLinearSpace by C0SP1:7;
for v being Element of (RAlgebra Omega) st v in Real-Valued-Random-Variables-Set Sigma holds
- v in Real-Valued-Random-Variables-Set Sigma

proof

let v be Element of (RAlgebra Omega); :: thesis: ( v in Real-Valued-Random-Variables-Set Sigma implies - v in Real-Valued-Random-Variables-Set Sigma )
assume v in Real-Valued-Random-Variables-Set Sigma ; :: thesis: - v in Real-Valued-Random-Variables-Set Sigma
then consider v1 being Real-Valued-Random-Variable of Sigma such that
A14: v1 = v ;
A15: - v1 is Real-Valued-Random-Variable of Sigma by RANDOM_1:20;
reconsider h = - v as Element of Funcs (Omega,REAL) ;
A16: h = (- 1) * v by A13, RLVECT_1:16;

A17: now :: thesis: for x being object st x in dom h holds
h . x = - (v1 . x)

let x be object ; :: thesis: ( x in dom h implies h . x = - (v1 . x) )
assume x in dom h ; :: thesis: h . x = - (v1 . x)
then reconsider y = x as Element of Omega ;
thus h . x = (- 1) * (v1 . y) by A16, A14, FUNCSDOM:4
.= - (v1 . x) ; :: thesis: verum

end;

( ex f being Function st
( h = f & dom f = Omega & rng f c= REAL ) & dom v1 = Omega ) by FUNCT_2:def 1, FUNCT_2:def 2;
then - v = - v1 by A17, VALUED_1:9;
hence - v in Real-Valued-Random-Variables-Set Sigma by A15; :: thesis: verum

end;

then A18: Real-Valued-Random-Variables-Set Sigma is having-inverse by C0SP1:def 1;
for a being Real
for u being Element of (RAlgebra Omega) st u in Real-Valued-Random-Variables-Set Sigma holds
a * u in Real-Valued-Random-Variables-Set Sigma

proof

let a be Real; :: thesis: for u being Element of (RAlgebra Omega) st u in Real-Valued-Random-Variables-Set Sigma holds
a * u in Real-Valued-Random-Variables-Set Sigma
let u be Element of (RAlgebra Omega); :: thesis: ( u in Real-Valued-Random-Variables-Set Sigma implies a * u in Real-Valued-Random-Variables-Set Sigma )
assume u in Real-Valued-Random-Variables-Set Sigma ; :: thesis: a * u in Real-Valued-Random-Variables-Set Sigma
then consider u1 being Real-Valued-Random-Variable of Sigma such that
A19: u1 = u ;
reconsider h = a * u as Element of Funcs (Omega,REAL) ;
A20: ( ex f being Function st
( h = f & dom f = Omega & rng f c= REAL ) & dom u1 = Omega ) by FUNCT_2:def 1, FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = a * (u1 . x) by A19, FUNCSDOM:4;
then a * u = a (#) u1 by A20, VALUED_1:def 5;
hence a * u in Real-Valued-Random-Variables-Set Sigma ; :: thesis: verum

end;

hence Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed by A12, A18, C0SP1:def 10; :: thesis: Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed
reconsider g = RealFuncUnit Omega as Function of Omega,REAL ;
g is Real-Valued-Random-Variable of Sigma by Th4;
then 1. (RAlgebra Omega) in Real-Valued-Random-Variables-Set Sigma ;
hence Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed by A1, C0SP1:def 4; :: thesis: verum