let v be VECTOR of (R_Algebra_of_Real-Valued-Random-Variables Sigma); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
reconsider v1 = v as VECTOR of (RAlgebra Omega) by TARSKI:def 3;
R_Algebra_of_Real-Valued-Random-Variables Sigma is Subalgebra of RAlgebra Omega by C0SP1:6;
then 1 * v = 1 * v1 by C0SP1:8;
hence 1 * v = v by FUNCSDOM:12; :: thesis: verum