let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of {1} st Omega = {1,2,3,4} holds
ex X1 being Function of Omega,{1} st
( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 )
let Sigma be SigmaField of Omega; :: thesis: for Sigma2 being SigmaField of {1} st Omega = {1,2,3,4} holds
ex X1 being Function of Omega,{1} st
( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 )
let Sigma2 be SigmaField of {1}; :: thesis: ( Omega = {1,2,3,4} implies ex X1 being Function of Omega,{1} st
( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 ) )
assume A1: Omega = {1,2,3,4} ; :: thesis: ex X1 being Function of Omega,{1} st
( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 )
reconsider 1REAL = 1 as Real ;
consider X1 being Function of Omega,{1REAL} such that
F4: X1 = Omega --> 1REAL ;
reconsider X1 = X1 as Function of Omega,{1} ;
take X1 ; :: thesis: ( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 )
thus ( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 ) by A1, Lm2A, F4; :: thesis: verum