:: RANDOM_2 semantic presentation
begin
theorem Th1: :: RANDOM_2:1
for f being one-to-one Function
for A, B being Subset of (dom f) st A misses B holds
rng (f | A) misses rng (f | B)
proof
let f be one-to-one Function; ::_thesis: for A, B being Subset of (dom f) st A misses B holds
rng (f | A) misses rng (f | B)
let A, B be Subset of (dom f); ::_thesis: ( A misses B implies rng (f | A) misses rng (f | B) )
assume A1: A misses B ; ::_thesis: rng (f | A) misses rng (f | B)
assume rng (f | A) meets rng (f | B) ; ::_thesis: contradiction
then consider y being set such that
A2: ( y in rng (f | A) & y in rng (f | B) ) by XBOOLE_0:3;
consider xa being set such that
A3: ( xa in dom (f | A) & y = (f | A) . xa ) by A2, FUNCT_1:def_3;
consider xb being set such that
A4: ( xb in dom (f | B) & y = (f | B) . xb ) by A2, FUNCT_1:def_3;
A5: ( xa in dom f & xb in dom f ) by A3, A4, RELAT_1:57;
( y = f . xa & y = f . xb ) by A3, A4, FUNCT_1:47;
then A6: xa = xb by A5, FUNCT_1:def_4;
( dom (f | A) c= A & dom (f | B) c= B ) by RELAT_1:58;
then xa in A /\ B by A6, A3, A4, XBOOLE_0:def_4;
hence contradiction by A1, XBOOLE_0:4; ::_thesis: verum
end;
theorem Th2: :: RANDOM_2:2
for f, g being Function holds rng (f * g) c= rng (f | (rng g))
proof
let f, g be Function; ::_thesis: rng (f * g) c= rng (f | (rng g))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f * g) or y in rng (f | (rng g)) )
assume y in rng (f * g) ; ::_thesis: y in rng (f | (rng g))
then consider x being set such that
A1: ( x in dom (f * g) & y = (f * g) . x ) by FUNCT_1:def_3;
A2: ( x in dom g & g . x in dom f ) by A1, FUNCT_1:11;
reconsider z = g . x as set ;
f . z in rng (f | (rng g)) by A2, FUNCT_1:3, FUNCT_1:50;
hence y in rng (f | (rng g)) by A1, FUNCT_1:12; ::_thesis: verum
end;
registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative for Real-Valued-Random-Variable of Sigma;
existence
ex b1 being Real-Valued-Random-Variable of Sigma st b1 is nonnegative
proof
set X = the Real-Valued-Random-Variable of Sigma;
now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_the_Real-Valued-Random-Variable_of_Sigma)_holds_
0_<=_(abs_the_Real-Valued-Random-Variable_of_Sigma)_._x
let x be set ; ::_thesis: ( x in dom (abs the Real-Valued-Random-Variable of Sigma) implies 0 <= (abs the Real-Valued-Random-Variable of Sigma) . x )
assume x in dom (abs the Real-Valued-Random-Variable of Sigma) ; ::_thesis: 0 <= (abs the Real-Valued-Random-Variable of Sigma) . x
then (abs the Real-Valued-Random-Variable of Sigma) . x = abs ( the Real-Valued-Random-Variable of Sigma . x) by VALUED_1:def_11;
hence 0 <= (abs the Real-Valued-Random-Variable of Sigma) . x by COMPLEX1:46; ::_thesis: verum
end;
then abs the Real-Valued-Random-Variable of Sigma is nonnegative by MESFUNC6:52;
hence ex b1 being Real-Valued-Random-Variable of Sigma st b1 is nonnegative ; ::_thesis: verum
end;
end;
registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let X be Real-Valued-Random-Variable of Sigma;
cluster|.X.| -> nonnegative ;
coherence
abs X is nonnegative
proof
now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_X)_holds_
0_<=_(abs_X)_._x
let x be set ; ::_thesis: ( x in dom (abs X) implies 0 <= (abs X) . x )
assume x in dom (abs X) ; ::_thesis: 0 <= (abs X) . x
then (abs X) . x = abs (X . x) by VALUED_1:def_11;
hence 0 <= (abs X) . x by COMPLEX1:46; ::_thesis: verum
end;
hence abs X is nonnegative by MESFUNC6:52; ::_thesis: verum
end;
end;
theorem Th3: :: RANDOM_2:3
for Omega being non empty set holds Omega --> 1 = chi (Omega,Omega)
proof
let Omega be non empty set ; ::_thesis: Omega --> 1 = chi (Omega,Omega)
set E0 = Omega --> 1;
A1: dom (chi (Omega,Omega)) = Omega by FUNCT_3:def_3;
A2: dom (Omega --> 1) = Omega by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(chi_(Omega,Omega))_holds_
(chi_(Omega,Omega))_._x_=_(Omega_-->_1)_._x
let x be set ; ::_thesis: ( x in dom (chi (Omega,Omega)) implies (chi (Omega,Omega)) . b1 = (Omega --> 1) . b1 )
assume A3: x in dom (chi (Omega,Omega)) ; ::_thesis: (chi (Omega,Omega)) . b1 = (Omega --> 1) . b1
percases ( x in Omega or not x in Omega ) ;
suppose x in Omega ; ::_thesis: (chi (Omega,Omega)) . b1 = (Omega --> 1) . b1
hence (chi (Omega,Omega)) . x = 1 by FUNCT_3:def_3
.= (Omega --> 1) . x by A3, FUNCOP_1:7 ;
::_thesis: verum
end;
suppose not x in Omega ; ::_thesis: (chi (Omega,Omega)) . b1 = (Omega --> 1) . b1
hence (chi (Omega,Omega)) . x = (Omega --> 1) . x by A3; ::_thesis: verum
end;
end;
end;
hence Omega --> 1 = chi (Omega,Omega) by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th4: :: RANDOM_2:4
for Omega being non empty set
for r being Real
for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma
proof
let Omega be non empty set ; ::_thesis: for r being Real
for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma
let r be Real; ::_thesis: for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; ::_thesis: Omega --> r is Real-Valued-Random-Variable of Sigma
set E0 = Omega --> 1;
set E = Omega --> r;
reconsider S = Omega as Element of Sigma by MEASURE1:7;
A1: ( dom (Omega --> 1) = Omega & rng (Omega --> 1) c= {1} ) by FUNCOP_1:13;
reconsider E0 = Omega --> 1 as Function of Omega,REAL by FUNCT_2:7;
A2: R_EAL E0 = chi (S,Omega) by Th3;
chi (S,Omega) is_measurable_on S by MESFUNC2:29;
then E0 is_measurable_on S by A2, MESFUNC6:def_1;
then A3: E0 is Real-Valued-Random-Variable of Sigma by RANDOM_1:def_2;
A4: dom (Omega --> r) = dom E0 by A1, FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Omega_-->_r)_holds_
(Omega_-->_r)_._x_=_r_*_(E0_._x)
let x be set ; ::_thesis: ( x in dom (Omega --> r) implies (Omega --> r) . x = r * (E0 . x) )
assume A5: x in dom (Omega --> r) ; ::_thesis: (Omega --> r) . x = r * (E0 . x)
hence (Omega --> r) . x = r * 1 by FUNCOP_1:7
.= r * (E0 . x) by A5, FUNCOP_1:7 ;
::_thesis: verum
end;
then Omega --> r = r (#) E0 by A4, VALUED_1:def_5;
hence Omega --> r is Real-Valued-Random-Variable of Sigma by A3, RANDOM_1:20; ::_thesis: verum
end;
theorem Th5: :: RANDOM_2:5
for X being non empty set
for f being PartFunc of X,REAL holds
( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds
( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )
let f be PartFunc of X,REAL; ::_thesis: ( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )
dom (- f) = dom f by VALUED_1:8;
then dom ((- f) to_power 2) = dom f by MESFUN6C:def_4;
then A1: dom (f to_power 2) = dom ((- f) to_power 2) by MESFUN6C:def_4;
dom (abs f) = dom f by VALUED_1:def_11;
then A2: dom ((abs f) to_power 2) = dom f by MESFUN6C:def_4;
then A3: dom (f to_power 2) = dom ((abs f) to_power 2) by MESFUN6C:def_4;
for x being Element of X st x in dom (f to_power 2) holds
( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x )
proof
let x be Element of X; ::_thesis: ( x in dom (f to_power 2) implies ( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x ) )
assume A4: x in dom (f to_power 2) ; ::_thesis: ( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x )
then A5: ( x in dom ((- f) to_power 2) & x in dom (f to_power 2) & x in dom f & x in dom (- f) & x in dom ((abs f) to_power 2) ) by A2, A1, MESFUN6C:def_4;
A6: ((- f) to_power 2) . x = ((- f) . x) to_power 2 by A4, A1, MESFUN6C:def_4
.= (- (f . x)) to_power 2 by VALUED_1:8
.= (f . x) to_power 2 by FIB_NUM3:3
.= (f to_power 2) . x by A4, MESFUN6C:def_4 ;
((abs f) to_power 2) . x = (f to_power 2) . x
proof
A7: ((abs f) to_power 2) . x = ((abs f) . x) to_power 2 by A5, MESFUN6C:def_4
.= (abs (f . x)) to_power 2 by VALUED_1:18 ;
now__::_thesis:_(_(_((abs_f)_to_power_2)_._x_=_(f_._x)_to_power_2_&_((abs_f)_to_power_2)_._x_=_(f_to_power_2)_._x_)_or_(_((abs_f)_to_power_2)_._x_=_(-_(f_._x))_to_power_2_&_((abs_f)_to_power_2)_._x_=_(f_to_power_2)_._x_)_)
percases ( ((abs f) to_power 2) . x = (f . x) to_power 2 or ((abs f) to_power 2) . x = (- (f . x)) to_power 2 ) by A7, ABSVALUE:1;
case ((abs f) to_power 2) . x = (f . x) to_power 2 ; ::_thesis: ((abs f) to_power 2) . x = (f to_power 2) . x
hence ((abs f) to_power 2) . x = (f to_power 2) . x by A4, MESFUN6C:def_4; ::_thesis: verum
end;
case ((abs f) to_power 2) . x = (- (f . x)) to_power 2 ; ::_thesis: ((abs f) to_power 2) . x = (f to_power 2) . x
then ((abs f) to_power 2) . x = (f . x) to_power 2 by FIB_NUM3:3
.= (f to_power 2) . x by A4, MESFUN6C:def_4 ;
hence ((abs f) to_power 2) . x = (f to_power 2) . x ; ::_thesis: verum
end;
end;
end;
hence ((abs f) to_power 2) . x = (f to_power 2) . x ; ::_thesis: verum
end;
hence ( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x ) by A6; ::_thesis: verum
end;
then ( ( for x being Element of X st x in dom (f to_power 2) holds
(f to_power 2) . x = ((- f) to_power 2) . x ) & ( for x being Element of X st x in dom (f to_power 2) holds
(f to_power 2) . x = ((abs f) to_power 2) . x ) ) ;
hence ( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 ) by A1, A3, PARTFUN1:5; ::_thesis: verum
end;
theorem Th6: :: RANDOM_2:6
for X being non empty set
for f, g being PartFunc of X,REAL holds
( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds
( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
let f, g be PartFunc of X,REAL; ::_thesis: ( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
A1: ( dom (f to_power 2) = dom f & ( for x being Element of X st x in dom (f to_power 2) holds
(f to_power 2) . x = (f . x) to_power 2 ) ) by MESFUN6C:def_4;
A2: ( dom (g to_power 2) = dom g & ( for x being Element of X st x in dom (g to_power 2) holds
(g to_power 2) . x = (g . x) to_power 2 ) ) by MESFUN6C:def_4;
A3: dom (2 (#) (f (#) g)) = dom (f (#) g) by VALUED_1:def_5
.= (dom f) /\ (dom g) by VALUED_1:def_4 ;
A4: now__::_thesis:_for_x_being_Element_of_X_st_x_in_(dom_f)_/\_(dom_g)_holds_
(2_(#)_(f_(#)_g))_._x_=_(2_*_(f_._x))_*_(g_._x)
let x be Element of X; ::_thesis: ( x in (dom f) /\ (dom g) implies (2 (#) (f (#) g)) . x = (2 * (f . x)) * (g . x) )
assume x in (dom f) /\ (dom g) ; ::_thesis: (2 (#) (f (#) g)) . x = (2 * (f . x)) * (g . x)
thus (2 (#) (f (#) g)) . x = 2 * ((f (#) g) . x) by VALUED_1:6
.= 2 * ((f . x) * (g . x)) by VALUED_1:5
.= (2 * (f . x)) * (g . x) ; ::_thesis: verum
end;
A5: dom ((f + g) to_power 2) = dom (f + g) by MESFUN6C:def_4
.= (dom f) /\ (dom g) by VALUED_1:def_1 ;
A6: dom ((f - g) to_power 2) = dom (f - g) by MESFUN6C:def_4
.= (dom f) /\ (dom g) by VALUED_1:12 ;
A7: dom ((f to_power 2) + (2 (#) (f (#) g))) = (dom f) /\ (dom (2 (#) (f (#) g))) by A1, VALUED_1:def_1
.= (dom f) /\ (dom g) by A3, XBOOLE_1:17, XBOOLE_1:28 ;
A8: dom ((f to_power 2) - (2 (#) (f (#) g))) = (dom f) /\ (dom (2 (#) (f (#) g))) by A1, VALUED_1:12
.= (dom f) /\ (dom g) by A3, XBOOLE_1:17, XBOOLE_1:28 ;
A9: dom (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) = (dom ((f to_power 2) + (2 (#) (f (#) g)))) /\ (dom g) by A2, VALUED_1:def_1
.= ((dom f) /\ (dom (2 (#) (f (#) g)))) /\ (dom g) by A1, VALUED_1:def_1
.= ((dom f) /\ (dom g)) /\ (dom g) by A3, XBOOLE_1:17, XBOOLE_1:28
.= (dom f) /\ (dom g) by XBOOLE_1:17, XBOOLE_1:28 ;
A10: dom (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) = (dom ((f to_power 2) - (2 (#) (f (#) g)))) /\ (dom g) by A2, VALUED_1:def_1
.= (dom f) /\ (dom g) by A8, XBOOLE_1:17, XBOOLE_1:28 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_(dom_f)_/\_(dom_g)_holds_
(_((f_+_g)_to_power_2)_._x_=_(((f_to_power_2)_+_(2_(#)_(f_(#)_g)))_+_(g_to_power_2))_._x_&_((f_-_g)_to_power_2)_._x_=_(((f_to_power_2)_-_(2_(#)_(f_(#)_g)))_+_(g_to_power_2))_._x_)
let x be Element of X; ::_thesis: ( x in (dom f) /\ (dom g) implies ( ((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x & ((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x ) )
assume A11: x in (dom f) /\ (dom g) ; ::_thesis: ( ((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x & ((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x )
then A12: x in dom (f + g) by VALUED_1:def_1;
A13: x in dom f by A11, XBOOLE_0:def_4;
A14: x in dom g by A11, XBOOLE_0:def_4;
A15: x in dom (f - g) by A11, VALUED_1:12;
then A16: x in dom ((f - g) to_power 2) by MESFUN6C:def_4;
A17: ((f + g) to_power 2) . x = ((f + g) . x) to_power 2 by A11, A5, MESFUN6C:def_4
.= ((f . x) + (g . x)) to_power 2 by A12, VALUED_1:def_1
.= ((f . x) + (g . x)) ^2 by POWER:46
.= (((f . x) ^2) + ((2 * (f . x)) * (g . x))) + ((g . x) ^2)
.= (((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) ^2) by POWER:46
.= (((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by POWER:46
.= (((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by A1, A13
.= (((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x) by A2, A14
.= (((f to_power 2) . x) + ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x) by A4, A11
.= (((f to_power 2) + (2 (#) (f (#) g))) . x) + ((g to_power 2) . x) by A7, A11, VALUED_1:def_1
.= (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x by A9, A11, VALUED_1:def_1 ;
((f - g) to_power 2) . x = ((f - g) . x) to_power 2 by A16, MESFUN6C:def_4
.= ((f . x) - (g . x)) to_power 2 by A15, VALUED_1:13
.= ((f . x) - (g . x)) ^2 by POWER:46
.= (((f . x) ^2) - ((2 * (f . x)) * (g . x))) + ((g . x) ^2)
.= (((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) ^2) by POWER:46
.= (((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by POWER:46
.= (((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by A1, A13
.= (((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x) by A2, A14
.= (((f to_power 2) . x) - ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x) by A4, A11
.= (((f to_power 2) - (2 (#) (f (#) g))) . x) + ((g to_power 2) . x) by A8, A11, VALUED_1:13
.= (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x by A10, A11, VALUED_1:def_1 ;
hence ( ((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x & ((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x ) by A17; ::_thesis: verum
end;
then ( ( for x being Element of X st x in dom ((f + g) to_power 2) holds
((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x ) & ( for x being Element of X st x in dom ((f - g) to_power 2) holds
((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x ) ) by A5, A6;
hence ( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) ) by A5, A9, A10, A6, PARTFUN1:5; ::_thesis: verum
end;
definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let X be Real-Valued-Random-Variable of Sigma;
assume A1: ( X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ;
func variance (X,P) -> Element of REAL means :Def1: :: RANDOM_2:def 1
ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & it = Integral ((P2M P),((abs Y) to_power 2)) );
correctness
existence
ex b1 being Element of REAL ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) );
uniqueness
for b1, b2 being Element of REAL st ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) ) & ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b2 = Integral ((P2M P),((abs Y) to_power 2)) ) holds
b1 = b2;
proof
consider S being Element of Sigma such that
A2: ( S = Omega & X is_measurable_on S ) by RANDOM_1:def_2;
(P2M P) . S <= 1 by PROB_1:35;
then A3: (P2M P) . S < +infty by XXREAL_0:2, XXREAL_0:9;
set r = expect (X,P);
set E0 = Omega --> 1;
set E = Omega --> (expect (X,P));
A4: ( dom (Omega --> 1) = Omega & rng (Omega --> 1) c= {1} ) by FUNCOP_1:13;
reconsider E0 = Omega --> 1 as Real-Valued-Random-Variable of Sigma by Th4;
A5: R_EAL E0 = chi (S,Omega) by A2, Th3;
A6: dom (Omega --> (expect (X,P))) = dom E0 by A4, FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Omega_-->_(expect_(X,P)))_holds_
(Omega_-->_(expect_(X,P)))_._x_=_(expect_(X,P))_*_(E0_._x)
let x be set ; ::_thesis: ( x in dom (Omega --> (expect (X,P))) implies (Omega --> (expect (X,P))) . x = (expect (X,P)) * (E0 . x) )
assume A7: x in dom (Omega --> (expect (X,P))) ; ::_thesis: (Omega --> (expect (X,P))) . x = (expect (X,P)) * (E0 . x)
hence (Omega --> (expect (X,P))) . x = (expect (X,P)) * 1 by FUNCOP_1:7
.= (expect (X,P)) * (E0 . x) by A7, FUNCOP_1:7 ;
::_thesis: verum
end;
then A8: Omega --> (expect (X,P)) = (expect (X,P)) (#) E0 by A6, VALUED_1:def_5;
reconsider E = Omega --> (expect (X,P)) as Real-Valued-Random-Variable of Sigma by Th4;
set Y = X - E;
reconsider Y = X - E as Real-Valued-Random-Variable of Sigma ;
chi (S,Omega) is_integrable_on P2M P by A3, MESFUNC7:24;
then A9: E0 is_integrable_on P2M P by A5, MESFUNC6:def_4;
then A10: (expect (X,P)) (#) E0 is_integrable_on P2M P by MESFUNC6:102;
A11: - 1 is Real by XREAL_0:def_1;
then A12: (- 1) (#) ((expect (X,P)) (#) E0) is_integrable_on P2M P by A10, MESFUNC6:102;
A13: X is_integrable_on P2M P by A1, RANDOM_1:def_3;
then Y is_integrable_on P2M P by A8, A12, MESFUNC6:100;
then A14: Y is_integrable_on P by RANDOM_1:def_3;
(2 * (expect (X,P))) (#) X is_integrable_on P2M P by A13, MESFUNC6:102;
then (- 1) (#) ((2 * (expect (X,P))) (#) X) is_integrable_on P2M P by A11, MESFUNC6:102;
then A15: ((abs X) to_power 2) - ((2 * (expect (X,P))) (#) X) is_integrable_on P2M P by A1, MESFUNC6:100;
A16: ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) = ((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)
proof
A17: dom (X to_power 2) = dom X by MESFUN6C:def_4;
A18: dom (2 (#) (((expect (X,P)) (#) E0) (#) X)) = dom (((expect (X,P)) (#) E0) (#) X) by VALUED_1:def_5
.= (dom ((expect (X,P)) (#) E0)) /\ (dom X) by VALUED_1:def_4
.= Omega /\ (dom X) by A4, VALUED_1:def_5 ;
A19: dom (((expect (X,P)) (#) E0) to_power 2) = dom ((expect (X,P)) (#) E0) by MESFUN6C:def_4
.= Omega by A4, VALUED_1:def_5 ;
A20: dom (((expect (X,P)) * (expect (X,P))) (#) E0) = Omega by A4, VALUED_1:def_5;
A21: dom ((2 * (expect (X,P))) (#) X) = dom X by VALUED_1:def_5;
A22: dom ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) = (dom X) /\ (Omega /\ (dom X)) by A17, A18, VALUED_1:12
.= ((dom X) /\ (dom X)) /\ Omega by XBOOLE_1:16
.= (dom X) /\ Omega ;
A23: dom ((X to_power 2) - ((2 * (expect (X,P))) (#) X)) = (dom (X to_power 2)) /\ (dom ((2 * (expect (X,P))) (#) X)) by VALUED_1:12
.= dom X by A17, A21 ;
A24: dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) = (dom ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X)))) /\ (dom (((expect (X,P)) (#) E0) to_power 2)) by VALUED_1:def_1
.= (dom X) /\ (Omega /\ Omega) by A19, A22, XBOOLE_1:16
.= (dom X) /\ Omega ;
then A25: dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) = dom (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) by A20, A23, VALUED_1:def_1;
for x being Element of Omega st x in dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) holds
(((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x
proof
let x be Element of Omega; ::_thesis: ( x in dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) implies (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x )
assume A26: x in dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) ; ::_thesis: (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x
then A27: ( x in dom X & x in Omega ) by A24, XBOOLE_0:def_4;
A28: (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) . x) + ((((expect (X,P)) (#) E0) to_power 2) . x) by A26, VALUED_1:def_1
.= (((X to_power 2) . x) - ((2 (#) (((expect (X,P)) (#) E0) (#) X)) . x)) + ((((expect (X,P)) (#) E0) to_power 2) . x) by A22, A24, A26, VALUED_1:13
.= (((X to_power 2) . x) - (2 * ((((expect (X,P)) (#) E0) (#) X) . x))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:6
.= (((X to_power 2) . x) - (2 * ((((expect (X,P)) (#) E0) . x) * (X . x)))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:5
.= (((X to_power 2) . x) - (2 * (((expect (X,P)) * (E0 . x)) * (X . x)))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:6
.= (((X to_power 2) . x) - (2 * (((expect (X,P)) * 1) * (X . x)))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by FUNCOP_1:7
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((((expect (X,P)) (#) E0) . x) to_power 2) by A19, MESFUN6C:def_4
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * (E0 . x)) to_power 2) by VALUED_1:6
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * 1) to_power 2) by FUNCOP_1:7
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) ^2) by POWER:46
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) * (expect (X,P))) ;
(((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) . x) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by A26, A25, VALUED_1:def_1
.= (((X to_power 2) . x) - (((2 * (expect (X,P))) (#) X) . x)) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by A23, A27, VALUED_1:13
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by VALUED_1:6
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * (expect (X,P))) * (E0 . x)) by VALUED_1:6
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * (expect (X,P))) * 1) by FUNCOP_1:7
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) * (expect (X,P))) ;
hence (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x by A28; ::_thesis: verum
end;
hence ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) = ((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0) by A25, PARTFUN1:5; ::_thesis: verum
end;
A29: (abs Y) to_power 2 = (X - ((expect (X,P)) (#) E0)) to_power 2 by Th5, A8
.= ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) by Th6
.= (((abs X) to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0) by Th5, A16 ;
A30: ((expect (X,P)) * (expect (X,P))) (#) E0 is_integrable_on P2M P by A9, MESFUNC6:102;
then (abs Y) to_power 2 is_integrable_on P2M P by A15, A29, MESFUNC6:100;
then ( -infty < Integral ((P2M P),((abs Y) to_power 2)) & Integral ((P2M P),((abs Y) to_power 2)) < +infty ) by MESFUNC6:90;
then Integral ((P2M P),((abs Y) to_power 2)) is Element of REAL by XXREAL_0:14;
hence ( ex b1 being Element of REAL ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) ) & ( for b1, b2 being Element of REAL st ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) ) & ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b2 = Integral ((P2M P),((abs Y) to_power 2)) ) holds
b1 = b2 ) ) by A30, A15, A29, A14, MESFUNC6:100; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines variance RANDOM_2:def_1_:_
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for X being Real-Valued-Random-Variable of Sigma st X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
for b5 being Element of REAL holds
( b5 = variance (X,P) iff ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b5 = Integral ((P2M P),((abs Y) to_power 2)) ) );
begin
theorem :: RANDOM_2:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
let P be Probability of Sigma; ::_thesis: for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
let r be Real; ::_thesis: for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
let X be Real-Valued-Random-Variable of Sigma; ::_thesis: ( 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P implies P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2) )
assume A1: ( 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ; ::_thesis: P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
A2: { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } c= { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } or s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } )
assume s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } ; ::_thesis: s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 }
then A3: ex ss being Element of Omega st
( s = ss & r <= |.((X . ss) - (expect (X,P))).| ) ;
A4: ( r ^2 = r to_power 2 & (abs ((X . s) - (expect (X,P)))) ^2 = (abs ((X . s) - (expect (X,P)))) to_power 2 ) by POWER:46;
r ^2 <= (abs ((X . s) - (expect (X,P)))) ^2 by A1, A3, SQUARE_1:15;
hence s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } by A3, A4; ::_thesis: verum
end;
{ t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } c= { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } or s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } )
assume s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } ; ::_thesis: s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| }
then A5: ex ss being Element of Omega st
( s = ss & r to_power 2 <= (abs ((X . ss) - (expect (X,P)))) to_power 2 ) ;
A6: 0 <= abs ((X . s) - (expect (X,P))) by COMPLEX1:46;
( r ^2 = r to_power 2 & (abs ((X . s) - (expect (X,P)))) ^2 = (abs ((X . s) - (expect (X,P)))) to_power 2 ) by POWER:46;
then r <= abs ((X . s) - (expect (X,P))) by A6, A5, SQUARE_1:47;
hence s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } by A5; ::_thesis: verum
end;
then A7: { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } = { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } by A2, XBOOLE_0:def_10;
consider Y, E being Real-Valued-Random-Variable of Sigma such that
A8: ( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & variance (X,P) = Integral ((P2M P),((abs Y) to_power 2)) ) by Def1, A1;
reconsider Z = (abs Y) to_power 2 as Real-Valued-Random-Variable of Sigma by RANDOM_1:23;
A9: Z is_integrable_on P by A8, RANDOM_1:def_3;
then A10: P . { t where t is Element of Omega : r to_power 2 <= Z . t } <= (expect (Z,P)) / (r to_power 2) by A1, POWER:34, RANDOM_1:36;
A11: expect (Z,P) = variance (X,P) by A8, A9, RANDOM_1:def_4;
A12: dom X = Omega by FUNCT_2:def_1;
A13: dom (Omega --> (expect (X,P))) = Omega by FUNCOP_1:13;
A14: dom (X - (Omega --> (expect (X,P)))) = (dom X) /\ (dom (Omega --> (expect (X,P)))) by VALUED_1:12
.= Omega by A12, A13 ;
then A15: dom (abs (X - (Omega --> (expect (X,P))))) = Omega by VALUED_1:def_11;
then A16: dom ((abs (X - (Omega --> (expect (X,P))))) to_power 2) = Omega by MESFUN6C:def_4;
A17: { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } c= { t where t is Element of Omega : r to_power 2 <= Z . t }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } or s in { t where t is Element of Omega : r to_power 2 <= Z . t } )
assume s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } ; ::_thesis: s in { t where t is Element of Omega : r to_power 2 <= Z . t }
then A18: ex ss being Element of Omega st
( s = ss & r to_power 2 <= (abs ((X . ss) - (expect (X,P)))) to_power 2 ) ;
then Z . s = ((abs (X - (Omega --> (expect (X,P))))) . s) to_power 2 by A16, A8, MESFUN6C:def_4
.= (abs ((X - (Omega --> (expect (X,P)))) . s)) to_power 2 by A15, A18, VALUED_1:def_11
.= (abs ((X . s) - ((Omega --> (expect (X,P))) . s))) to_power 2 by A14, A18, VALUED_1:13
.= (abs ((X . s) - (expect (X,P)))) to_power 2 by A18, FUNCOP_1:7 ;
hence s in { t where t is Element of Omega : r to_power 2 <= Z . t } by A18; ::_thesis: verum
end;
{ t where t is Element of Omega : r to_power 2 <= Z . t } c= { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { t where t is Element of Omega : r to_power 2 <= Z . t } or s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } )
assume s in { t where t is Element of Omega : r to_power 2 <= Z . t } ; ::_thesis: s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 }
then A19: ex ss being Element of Omega st
( s = ss & r to_power 2 <= Z . ss ) ;
then Z . s = ((abs (X - (Omega --> (expect (X,P))))) . s) to_power 2 by A16, A8, MESFUN6C:def_4
.= (abs ((X - (Omega --> (expect (X,P)))) . s)) to_power 2 by A15, A19, VALUED_1:def_11
.= (abs ((X . s) - ((Omega --> (expect (X,P))) . s))) to_power 2 by A14, A19, VALUED_1:13
.= (abs ((X . s) - (expect (X,P)))) to_power 2 by A19, FUNCOP_1:7 ;
hence s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect (X,P)))) to_power 2 } by A19; ::_thesis: verum
end;
hence P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2) by A11, A10, A7, A17, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem Th8: :: RANDOM_2:8
for Omega being non empty finite set
for f being Function of Omega,REAL
for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds
P is Probability of Trivial-SigmaField Omega
proof
let Omega be non empty finite set ; ::_thesis: for f being Function of Omega,REAL
for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds
P is Probability of Trivial-SigmaField Omega
let f be Function of Omega,REAL; ::_thesis: for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds
P is Probability of Trivial-SigmaField Omega
let P be Function of (bool Omega),REAL; ::_thesis: ( ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) implies P is Probability of Trivial-SigmaField Omega )
assume that
A1: for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) and
A2: P . Omega = 1 and
A3: for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ; ::_thesis: P is Probability of Trivial-SigmaField Omega
A4: for A, B being Event of Trivial-SigmaField Omega st A misses B holds
P . (A \/ B) = (P . A) + (P . B)
proof
let A, B be Event of Trivial-SigmaField Omega; ::_thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) )
assume A5: A misses B ; ::_thesis: P . (A \/ B) = (P . A) + (P . B)
reconsider A0 = A, B0 = B as finite Subset of Omega ;
A6: Omega = dom f by FUNCT_2:def_1;
thus P . (A \/ B) = setopfunc ((A0 \/ B0),Omega,REAL,f,addreal) by A3
.= addreal . ((setopfunc (A0,Omega,REAL,f,addreal)),(setopfunc (B0,Omega,REAL,f,addreal))) by A5, A6, BHSP_5:14
.= addreal . ((setopfunc (A0,Omega,REAL,f,addreal)),(P . B)) by A3
.= addreal . ((P . A),(P . B)) by A3
.= (P . A) + (P . B) by BINOP_2:def_9 ; ::_thesis: verum
end;
A7: for A being Event of Trivial-SigmaField Omega holds 0 <= P . A by A1;
for ASeq being SetSequence of Trivial-SigmaField Omega st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
proof
let ASeq be SetSequence of Trivial-SigmaField Omega; ::_thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
assume ASeq is non-ascending ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
then consider N being Element of NAT such that
A8: for m being Element of NAT st N <= m holds
Intersection ASeq = ASeq . m by RANDOM_1:15;
now__::_thesis:_for_m_being_Element_of_NAT_st_N_<=_m_holds_
(P_*_ASeq)_._m_=_P_._(Intersection_ASeq)
let m be Element of NAT ; ::_thesis: ( N <= m implies (P * ASeq) . m = P . (Intersection ASeq) )
assume A9: N <= m ; ::_thesis: (P * ASeq) . m = P . (Intersection ASeq)
m in NAT ;
then m in dom ASeq by FUNCT_2:def_1;
hence (P * ASeq) . m = P . (ASeq . m) by FUNCT_1:13
.= P . (Intersection ASeq) by A8, A9 ;
::_thesis: verum
end;
hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by PROB_1:1; ::_thesis: verum
end;
hence P is Probability of Trivial-SigmaField Omega by A7, A4, A2, PROB_1:def_8; ::_thesis: verum
end;
Lm1: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
deffunc H1( set , set ) -> Element of REAL = (P1 . {$1}) * (P2 . {$2});
consider f being Function such that
A1: ( dom f = [:Omega1,Omega2:] & ( for x, y being set st x in Omega1 & y in Omega2 holds
f . (x,y) = H1(x,y) ) ) from FUNCT_3:sch_2();
for z being set st z in [:Omega1,Omega2:] holds
f . z in REAL
proof
let z be set ; ::_thesis: ( z in [:Omega1,Omega2:] implies f . z in REAL )
assume z in [:Omega1,Omega2:] ; ::_thesis: f . z in REAL
then consider x, y being set such that
A2: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def_2;
f . z = f . (x,y) by A2
.= H1(x,y) by A1, A2 ;
hence f . z in REAL ; ::_thesis: verum
end;
then reconsider f = f as Function of [:Omega1,Omega2:],REAL by A1, FUNCT_2:3;
take f ; ::_thesis: for x, y being set st x in Omega1 & y in Omega2 holds
f . (x,y) = (P1 . {x}) * (P2 . {y})
thus for x, y being set st x in Omega1 & y in Omega2 holds
f . (x,y) = (P1 . {x}) * (P2 . {y}) by A1; ::_thesis: verum
end;
Lm2: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
let Q1, Q2 be Function of [:Omega1,Omega2:],REAL; ::_thesis: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) implies Q1 = Q2 )
assume A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) ) ; ::_thesis: Q1 = Q2
A2: ( dom Q1 = [:Omega1,Omega2:] & dom Q2 = [:Omega1,Omega2:] ) by FUNCT_2:def_1;
now__::_thesis:_for_z_being_set_st_z_in_dom_Q1_holds_
Q1_._z_=_Q2_._z
let z be set ; ::_thesis: ( z in dom Q1 implies Q1 . z = Q2 . z )
assume z in dom Q1 ; ::_thesis: Q1 . z = Q2 . z
then consider x, y being set such that
A3: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def_2;
thus Q1 . z = Q1 . (x,y) by A3
.= (P1 . {x}) * (P2 . {y}) by A3, A1
.= Q2 . (x,y) by A3, A1
.= Q2 . z by A3 ; ::_thesis: verum
end;
hence Q1 = Q2 by A2, FUNCT_1:2; ::_thesis: verum
end;
Lm3: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
let Q be Function of [:Omega1,Omega2:],REAL; ::_thesis: ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
defpred S1[ set , set ] means ex z being finite Subset of [:Omega1,Omega2:] st
( $1 = z & $2 = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) );
A1: for x being set st x in bool [:Omega1,Omega2:] holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in bool [:Omega1,Omega2:] implies ex y being set st
( y in REAL & S1[x,y] ) )
assume x in bool [:Omega1,Omega2:] ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider z = x as finite Subset of [:Omega1,Omega2:] ;
setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) in REAL ;
hence ex y being set st
( y in REAL & S1[x,y] ) ; ::_thesis: verum
end;
consider P being Function of (bool [:Omega1,Omega2:]),REAL such that
A2: for x being set st x in bool [:Omega1,Omega2:] holds
S1[x,P . x] from FUNCT_2:sch_1(A1);
take P ; ::_thesis: for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
thus for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ::_thesis: verum
proof
let z be finite Subset of [:Omega1,Omega2:]; ::_thesis: P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
ex z1 being finite Subset of [:Omega1,Omega2:] st
( z = z1 & P . z = setopfunc (z1,[:Omega1,Omega2:],REAL,Q,addreal) ) by A2;
hence P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ; ::_thesis: verum
end;
end;
Lm4: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
let Q be Function of [:Omega1,Omega2:],REAL; ::_thesis: for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
let P1, P2 be Function of (bool [:Omega1,Omega2:]),REAL; ::_thesis: ( ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) implies P1 = P2 )
assume A1: for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ; ::_thesis: ( ex z being finite Subset of [:Omega1,Omega2:] st not P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) or P1 = P2 )
assume A2: for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ; ::_thesis: P1 = P2
now__::_thesis:_for_x_being_set_st_x_in_bool_[:Omega1,Omega2:]_holds_
P1_._x_=_P2_._x
let x be set ; ::_thesis: ( x in bool [:Omega1,Omega2:] implies P1 . x = P2 . x )
assume x in bool [:Omega1,Omega2:] ; ::_thesis: P1 . x = P2 . x
then reconsider z = x as finite Subset of [:Omega1,Omega2:] ;
thus P1 . x = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= P2 . x by A2 ; ::_thesis: verum
end;
hence P1 = P2 by FUNCT_2:12; ::_thesis: verum
end;
Lm5: for DK, DX being non empty set
for F being Function of DX,DK
for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
proof
let DK, DX be non empty set ; ::_thesis: for F being Function of DX,DK
for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
let F be Function of DX,DK; ::_thesis: for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
let p, q be FinSequence of DX; ::_thesis: for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
let fp, fq be FinSequence of DK; ::_thesis: ( fp = F * p & fq = F * q implies F * (p ^ q) = fp ^ fq )
assume A1: ( fp = F * p & fq = F * q ) ; ::_thesis: F * (p ^ q) = fp ^ fq
then A2: ( dom fp = dom p & dom fq = dom q ) by FINSEQ_3:120;
A3: ( len fp = len p & len fq = len q ) by A1, FINSEQ_3:120;
then A4: dom (fp ^ fq) = Seg ((len p) + (len q)) by FINSEQ_1:def_7;
A5: dom (F * (p ^ q)) = dom (p ^ q) by FINSEQ_3:120
.= Seg ((len p) + (len q)) by FINSEQ_1:def_7 ;
for x being set st x in dom (F * (p ^ q)) holds
(fp ^ fq) . x = (F * (p ^ q)) . x
proof
let x be set ; ::_thesis: ( x in dom (F * (p ^ q)) implies (fp ^ fq) . x = (F * (p ^ q)) . x )
assume A6: x in dom (F * (p ^ q)) ; ::_thesis: (fp ^ fq) . x = (F * (p ^ q)) . x
then reconsider n = x as Element of NAT ;
A7: ( 1 <= n & n <= (len p) + (len q) ) by A6, A5, FINSEQ_1:1;
A8: (F * (p ^ q)) . n = F . ((p ^ q) . n) by A6, FINSEQ_3:120;
percases ( n <= len p or not n <= len p ) ;
suppose n <= len p ; ::_thesis: (fp ^ fq) . x = (F * (p ^ q)) . x
then n in Seg (len p) by A7;
then A9: n in dom p by FINSEQ_1:def_3;
hence (F * (p ^ q)) . x = F . (p . n) by A8, FINSEQ_1:def_7
.= fp . n by A1, A9, A2, FINSEQ_3:120
.= (fp ^ fq) . x by A9, A2, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA10: not n <= len p ; ::_thesis: (fp ^ fq) . x = (F * (p ^ q)) . x
then ( len p < n & n <= len (p ^ q) ) by A7, FINSEQ_1:22;
then A11: (p ^ q) . n = q . (n - (len p)) by FINSEQ_1:24;
A12: n - (len p) <= ((len p) + (len q)) - (len p) by A7, XREAL_1:9;
A13: (len p) - (len p) < n - (len p) by A10, XREAL_1:9;
then A14: n - (len p) is Element of NAT by INT_1:3;
then 1 <= n - (len p) by A13, NAT_1:14;
then n - (len p) in Seg (len q) by A12, A14;
then A15: n - (len p) in dom q by FINSEQ_1:def_3;
A16: ( len fp < n & n <= len (fp ^ fq) ) by A3, A10, A7, FINSEQ_1:22;
thus (F * (p ^ q)) . x = fq . (n - (len p)) by A1, A15, A2, A11, A8, FINSEQ_3:120
.= (fp ^ fq) . x by A16, A3, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
hence F * (p ^ q) = fp ^ fq by A4, A5, FUNCT_1:2; ::_thesis: verum
end;
theorem Th9: :: RANDOM_2:9
for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
proof
let DX be non empty set ; ::_thesis: for F being Function of DX,REAL
for Y being finite Subset of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
let F be Function of DX,REAL; ::_thesis: for Y being finite Subset of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
let Y be finite Subset of DX; ::_thesis: ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
dom F = DX by FUNCT_2:def_1;
then consider p being FinSequence of DX such that
A1: ( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = addreal "**" (Func_Seq (F,p)) ) by BHSP_5:def_5;
Sum (Func_Seq (F,p)) = addreal "**" (Func_Seq (F,p)) ;
hence ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) ) by A1; ::_thesis: verum
end;
theorem Th10: :: RANDOM_2:10
for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX
for p being FinSequence of DX st p is one-to-one & rng p = Y holds
setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
proof
let DX be non empty set ; ::_thesis: for F being Function of DX,REAL
for Y being finite Subset of DX
for p being FinSequence of DX st p is one-to-one & rng p = Y holds
setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
let F be Function of DX,REAL; ::_thesis: for Y being finite Subset of DX
for p being FinSequence of DX st p is one-to-one & rng p = Y holds
setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
let Y be finite Subset of DX; ::_thesis: for p being FinSequence of DX st p is one-to-one & rng p = Y holds
setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
let p be FinSequence of DX; ::_thesis: ( p is one-to-one & rng p = Y implies setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
assume A1: ( p is one-to-one & rng p = Y ) ; ::_thesis: setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
dom F = DX by FUNCT_2:def_1;
hence setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) by A1, BHSP_5:def_5; ::_thesis: verum
end;
Lm6: for p being Function st dom p = Seg 1 holds
p = <*(p . 1)*>
proof
let p be Function; ::_thesis: ( dom p = Seg 1 implies p = <*(p . 1)*> )
assume A1: dom p = Seg 1 ; ::_thesis: p = <*(p . 1)*>
consider x being set such that
A2: x = p . 1 ;
A3: rng p = {x} by A2, A1, FINSEQ_1:2, FUNCT_1:4;
p is FinSequence-like by A1, FINSEQ_1:def_2;
then consider pp being FinSequence such that
A4: pp = p ;
thus p = <*(p . 1)*> by A2, A4, A3, A1, FINSEQ_1:38; ::_thesis: verum
end;
theorem Th11: :: RANDOM_2:11
for DX1, DX2 being non empty set
for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
proof
let DX1, DX2 be non empty set ; ::_thesis: for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let F1 be Function of DX1,REAL; ::_thesis: for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let F2 be Function of DX2,REAL; ::_thesis: for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let G be Function of [:DX1,DX2:],REAL; ::_thesis: for Y1 being non empty finite Subset of DX1
for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y1 be non empty finite Subset of DX1; ::_thesis: for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let p1 be FinSequence of DX1; ::_thesis: ( p1 is one-to-one & rng p1 = Y1 implies for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) )
assume A1: ( p1 is one-to-one & rng p1 = Y1 ) ; ::_thesis: for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
defpred S1[ Nat] means for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = $1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)));
consider erp1 being set such that
A2: erp1 in rng p1 by A1, XBOOLE_0:def_1;
A3: ex x being set st
( x in dom p1 & erp1 = p1 . x ) by A2, FUNCT_1:def_3;
A4: S1[ 0 ]
proof
let p2 be FinSequence of DX2; ::_thesis: for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = 0 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let p3 be FinSequence of [:DX1,DX2:]; ::_thesis: for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = 0 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y2 be non empty finite Subset of DX2; ::_thesis: for Y3 being finite Subset of [:DX1,DX2:] st len p2 = 0 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y3 be finite Subset of [:DX1,DX2:]; ::_thesis: ( len p2 = 0 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) implies Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) )
assume A5: ( len p2 = 0 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) ) ; ::_thesis: Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
then p2 = {} ;
hence Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A5; ::_thesis: verum
end;
A6: S1[1]
proof
let p2 be FinSequence of DX2; ::_thesis: for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let p3 be FinSequence of [:DX1,DX2:]; ::_thesis: for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y2 be non empty finite Subset of DX2; ::_thesis: for Y3 being finite Subset of [:DX1,DX2:] st len p2 = 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y3 be finite Subset of [:DX1,DX2:]; ::_thesis: ( len p2 = 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) implies Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) )
assume A7: ( len p2 = 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) ) ; ::_thesis: Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
then A8: p2 = <*(p2 . 1)*> by FINSEQ_1:40;
then A9: Y2 = {(p2 . 1)} by A7, FINSEQ_1:38;
set w = p2 . 1;
set z = (F2 * p2) . 1;
dom F2 = DX2 by FUNCT_2:def_1;
then rng p2 c= dom F2 ;
then dom (F2 * p2) = dom p2 by RELAT_1:27;
then A10: dom (F2 * p2) = Seg 1 by A8, FINSEQ_1:38;
then Func_Seq (F2,p2) = <*((F2 * p2) . 1)*> by Lm6;
then A11: Sum (Func_Seq (F2,p2)) = (F2 * p2) . 1 by RVSUM_1:73;
A12: Y3 = [:Y1,{(p2 . 1)}:] by A7, A8, FINSEQ_1:38;
A13: len p1 = card Y1 by A1, FINSEQ_4:62;
A14: len p3 = card (rng p3) by A7, FINSEQ_4:62
.= card Y1 by A12, A7, CARD_1:69 ;
A15: dom p1 = Seg (card Y1) by A13, FINSEQ_1:def_3
.= dom p3 by A14, FINSEQ_1:def_3 ;
deffunc H1( Nat) -> set = [(p1 . $1),(p2 . 1)];
consider q3 being FinSequence such that
A16: len q3 = len p3 and
A17: for k being Nat st k in dom q3 holds
q3 . k = H1(k) from FINSEQ_1:sch_2();
A18: dom q3 = Seg (len p3) by A16, FINSEQ_1:def_3;
A19: dom p3 = Seg (len p3) by FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_q3_holds_
q3_._k_in_[:Y1,Y2:]
let k be Nat; ::_thesis: ( k in dom q3 implies q3 . k in [:Y1,Y2:] )
assume A20: k in dom q3 ; ::_thesis: q3 . k in [:Y1,Y2:]
then A21: p1 . k in Y1 by A1, A18, A19, A15, FUNCT_1:3;
p2 . 1 in Y2 by A9, TARSKI:def_1;
then [(p1 . k),(p2 . 1)] in [:Y1,Y2:] by A21, ZFMISC_1:87;
hence q3 . k in [:Y1,Y2:] by A20, A17; ::_thesis: verum
end;
then q3 is FinSequence of [:Y1,Y2:] by FINSEQ_2:12;
then A22: rng q3 c= [:Y1,Y2:] by FINSEQ_1:def_4;
[:Y1,Y2:] c= [:DX1,DX2:] by ZFMISC_1:96;
then rng q3 c= [:DX1,DX2:] by A22, XBOOLE_1:1;
then reconsider q3 = q3 as FinSequence of [:DX1,DX2:] by FINSEQ_1:def_4;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_q3_&_x2_in_dom_q3_&_q3_._x1_=_q3_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 implies x1 = x2 )
assume A23: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 ) ; ::_thesis: x1 = x2
then A24: ( x1 in dom p1 & x2 in dom p1 ) by A16, A19, A15, FINSEQ_1:def_3;
reconsider n1 = x1, n2 = x2 as Element of NAT by A23;
[(p1 . n1),(p2 . 1)] = q3 . n1 by A17, A23
.= [(p1 . n2),(p2 . 1)] by A17, A23 ;
then p1 . n1 = p1 . n2 by XTUPLE_0:1;
hence x1 = x2 by A1, A24, FUNCT_1:def_4; ::_thesis: verum
end;
then A25: q3 is one-to-one by FUNCT_1:def_4;
A26: rng q3 = [:Y1,Y2:]
proof
now__::_thesis:_for_z_being_set_st_z_in_[:Y1,Y2:]_holds_
z_in_rng_q3
let z be set ; ::_thesis: ( z in [:Y1,Y2:] implies z in rng q3 )
assume z in [:Y1,Y2:] ; ::_thesis: z in rng q3
then consider y1, y2 being set such that
A27: ( y1 in Y1 & y2 in Y2 & z = [y1,y2] ) by ZFMISC_1:def_2;
consider n1 being set such that
A28: ( n1 in dom p1 & y1 = p1 . n1 ) by A1, A27, FUNCT_1:def_3;
reconsider n1 = n1 as Element of NAT by A28;
A29: n1 in dom q3 by A28, A16, A19, A15, FINSEQ_1:def_3;
y2 = p2 . 1 by A9, A27, TARSKI:def_1;
then q3 . n1 = z by A27, A28, A17, A29;
hence z in rng q3 by A29, FUNCT_1:3; ::_thesis: verum
end;
then [:Y1,Y2:] c= rng q3 by TARSKI:def_3;
hence rng q3 = [:Y1,Y2:] by A22, XBOOLE_0:def_10; ::_thesis: verum
end;
then consider P being Permutation of (dom p3) such that
A30: ( q3 = p3 * P & dom P = dom p3 & rng P = dom p3 ) by A25, A7, BHSP_5:1;
A31: Func_Seq (G,q3) = (Func_Seq (G,p3)) * P by A30, RELAT_1:36;
dom G = [:DX1,DX2:] by FUNCT_2:def_1;
then rng p3 c= dom G ;
then dom (Func_Seq (G,p3)) = dom p3 by RELAT_1:27;
then A32: Sum (Func_Seq (G,q3)) = Sum (Func_Seq (G,p3)) by A31, FINSOP_1:7;
A33: dom G = [:DX1,DX2:] by FUNCT_2:def_1;
dom F1 = DX1 by FUNCT_2:def_1;
then A34: dom (F1 * p1) = dom p1 by A1, RELAT_1:27
.= Seg (len p1) by FINSEQ_1:def_3 ;
A35: dom (G * q3) = dom q3 by A33, A26, RELAT_1:27
.= Seg (len p1) by A13, A14, A16, FINSEQ_1:def_3 ;
then A36: dom (G * q3) = dom (((F2 * p2) . 1) (#) (F1 * p1)) by A34, VALUED_1:def_5;
now__::_thesis:_for_x_being_set_st_x_in_dom_(G_*_q3)_holds_
(G_*_q3)_._x_=_(((F2_*_p2)_._1)_(#)_(F1_*_p1))_._x
let x be set ; ::_thesis: ( x in dom (G * q3) implies (G * q3) . x = (((F2 * p2) . 1) (#) (F1 * p1)) . x )
assume A37: x in dom (G * q3) ; ::_thesis: (G * q3) . x = (((F2 * p2) . 1) (#) (F1 * p1)) . x
then reconsider nx = x as Element of NAT ;
dom (G * q3) = dom q3 by A33, A26, RELAT_1:27
.= Seg (len q3) by FINSEQ_1:def_3 ;
then A38: nx in dom q3 by A37, FINSEQ_1:def_3;
( 1 <= nx & nx <= len p1 ) by A37, A35, FINSEQ_1:1;
then A39: p1 /. nx = p1 . nx by FINSEQ_4:15;
A40: q3 . nx = [(p1 . nx),(p2 . 1)] by A17, A38;
A41: nx in dom p1 by A37, A35, FINSEQ_1:def_3;
then A42: q3 . nx = [(p1 /. nx),(p2 . 1)] by A40, PARTFUN1:def_6;
p1 . nx in Y1 by A41, A1, FUNCT_1:3;
then A43: ( p1 /. nx in Y1 & p2 . 1 in Y2 ) by A41, A9, PARTFUN1:def_6, TARSKI:def_1;
1 in dom (F2 * p2) by A10;
then A44: (F2 * p2) . 1 = F2 . (p2 . 1) by FUNCT_1:12;
thus (G * q3) . x = G . ((p1 /. nx),(p2 . 1)) by A42, A37, FUNCT_1:12
.= (F1 . (p1 /. nx)) * ((F2 * p2) . 1) by A44, A7, A43
.= ((F1 * p1) . nx) * ((F2 * p2) . 1) by A39, A35, A34, A37, FUNCT_1:12
.= (((F2 * p2) . 1) (#) (F1 * p1)) . x by VALUED_1:6 ; ::_thesis: verum
end;
then Func_Seq (G,q3) = ((F2 * p2) . 1) * (Func_Seq (F1,p1)) by A36, FUNCT_1:2;
hence Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A11, A32, RVSUM_1:87; ::_thesis: verum
end;
A45: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A46: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_(_(_n_=_0_&_S1[n_+_1]_)_or_(_n_>_0_&_S1[n_+_1]_)_)
percases ( n = 0 or n > 0 ) ;
case n = 0 ; ::_thesis: S1[n + 1]
hence S1[n + 1] by A6; ::_thesis: verum
end;
caseA47: n > 0 ; ::_thesis: S1[n + 1]
now__::_thesis:_for_p2_being_FinSequence_of_DX2
for_p3_being_FinSequence_of_[:DX1,DX2:]
for_Y2_being_non_empty_finite_Subset_of_DX2
for_Y3_being_finite_Subset_of_[:DX1,DX2:]_st_len_p2_=_n_+_1_&_p2_is_one-to-one_&_rng_p2_=_Y2_&_p3_is_one-to-one_&_rng_p3_=_Y3_&_Y3_=_[:Y1,Y2:]_&_(_for_x,_y_being_set_st_x_in_Y1_&_y_in_Y2_holds_
G_._(x,y)_=_(F1_._x)_*_(F2_._y)_)_holds_
Sum_(Func_Seq_(G,p3))_=_(Sum_(Func_Seq_(F1,p1)))_*_(Sum_(Func_Seq_(F2,p2)))
let p2 be FinSequence of DX2; ::_thesis: for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = n + 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let p3 be FinSequence of [:DX1,DX2:]; ::_thesis: for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = n + 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y2 be non empty finite Subset of DX2; ::_thesis: for Y3 being finite Subset of [:DX1,DX2:] st len p2 = n + 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y3 be finite Subset of [:DX1,DX2:]; ::_thesis: ( len p2 = n + 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) implies Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) )
assume A48: ( len p2 = n + 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) ) ; ::_thesis: Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
set lb = len p1;
set la = len p2;
deffunc H1( Nat) -> set = [(p1 . ((($1 -' 1) mod (len p1)) + 1)),(p2 . ((($1 -' 1) div (len p1)) + 1))];
consider FG being FinSequence such that
A49: len FG = (len p2) * (len p1) and
A50: for k being Nat st k in dom FG holds
FG . k = H1(k) from FINSEQ_1:sch_2();
A51: dom FG = Seg ((len p2) * (len p1)) by A49, FINSEQ_1:def_3;
A52: dom p1 = Seg (len p1) by FINSEQ_1:def_3;
A53: now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_
(_((k_-'_1)_div_(len_p1))_+_1_in_dom_p2_&_((k_-'_1)_mod_(len_p1))_+_1_in_dom_p1_)
reconsider lap = len p2, lbp = len p1 as Nat ;
let k be Nat; ::_thesis: ( k in dom FG implies ( ((k -' 1) div (len p1)) + 1 in dom p2 & ((k -' 1) mod (len p1)) + 1 in dom p1 ) )
set i = ((k -' 1) div (len p1)) + 1;
set j = ((k -' 1) mod (len p1)) + 1;
assume k in dom FG ; ::_thesis: ( ((k -' 1) div (len p1)) + 1 in dom p2 & ((k -' 1) mod (len p1)) + 1 in dom p1 )
then A54: k in Seg ((len p2) * (len p1)) by A49, FINSEQ_1:def_3;
then A55: k <= (len p2) * (len p1) by FINSEQ_1:1;
then k -' 1 <= ((len p2) * (len p1)) -' 1 by NAT_D:42;
then A56: (k -' 1) div (len p1) <= (((len p2) * (len p1)) -' 1) div (len p1) by NAT_2:24;
1 <= k by A54, FINSEQ_1:1;
then A57: ( lbp divides lap * lbp & 1 <= (len p2) * (len p1) ) by A55, NAT_D:def_3, XXREAL_0:2;
A58: len p1 <> 0 by A54;
then len p1 >= 0 + 1 by NAT_1:13;
then ((lap * lbp) -' 1) div lbp = ((lap * lbp) div lbp) - 1 by A57, NAT_2:15;
then A59: ((k -' 1) div (len p1)) + 1 <= ((len p2) * (len p1)) div (len p1) by A56, XREAL_1:19;
reconsider la = len p2, lb = len p1 as Nat ;
( ((k -' 1) div (len p1)) + 1 >= 0 + 1 & ((k -' 1) div (len p1)) + 1 <= la ) by A58, A59, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len p1)) + 1 in Seg la ;
hence ((k -' 1) div (len p1)) + 1 in dom p2 by FINSEQ_1:def_3; ::_thesis: ((k -' 1) mod (len p1)) + 1 in dom p1
(k -' 1) mod lb < lb by A58, NAT_D:1;
then ( ((k -' 1) mod (len p1)) + 1 >= 0 + 1 & ((k -' 1) mod (len p1)) + 1 <= lb ) by NAT_1:13;
then ((k -' 1) mod (len p1)) + 1 in Seg lb ;
hence ((k -' 1) mod (len p1)) + 1 in dom p1 by FINSEQ_1:def_3; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_
FG_._k_in_[:DX1,DX2:]
let k be Nat; ::_thesis: ( k in dom FG implies FG . k in [:DX1,DX2:] )
set i = ((k -' 1) div (len p1)) + 1;
set j = ((k -' 1) mod (len p1)) + 1;
assume A60: k in dom FG ; ::_thesis: FG . k in [:DX1,DX2:]
then A61: p2 . (((k -' 1) div (len p1)) + 1) in rng p2 by A53, FUNCT_1:3;
p1 . (((k -' 1) mod (len p1)) + 1) in rng p1 by A53, A60, FUNCT_1:3;
then [(p1 . (((k -' 1) mod (len p1)) + 1)),(p2 . (((k -' 1) div (len p1)) + 1))] in [:DX1,DX2:] by A61, ZFMISC_1:87;
hence FG . k in [:DX1,DX2:] by A50, A60; ::_thesis: verum
end;
then reconsider q3 = FG as FinSequence of [:DX1,DX2:] by FINSEQ_2:12;
A62: len p1 = card Y1 by A1, FINSEQ_4:62;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_q3_&_x2_in_dom_q3_&_q3_._x1_=_q3_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 implies x1 = x2 )
assume A63: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 ) ; ::_thesis: x1 = x2
then A64: ( x1 in Seg (len q3) & x2 in Seg (len q3) ) by FINSEQ_1:def_3;
reconsider n1 = x1, n2 = x2 as Element of NAT by A63;
A65: q3 . n1 = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by A50, A63;
A66: q3 . n2 = [(p1 . (((n2 -' 1) mod (len p1)) + 1)),(p2 . (((n2 -' 1) div (len p1)) + 1))] by A50, A63;
then A67: p1 . (((n1 -' 1) mod (len p1)) + 1) = p1 . (((n2 -' 1) mod (len p1)) + 1) by A63, A65, XTUPLE_0:1;
( ((n1 -' 1) mod (len p1)) + 1 in dom p1 & ((n2 -' 1) mod (len p1)) + 1 in dom p1 ) by A63, A53;
then A68: ((n1 -' 1) mod (len p1)) + 1 = ((n2 -' 1) mod (len p1)) + 1 by A1, A67, FUNCT_1:def_4;
A69: p2 . (((n1 -' 1) div (len p1)) + 1) = p2 . (((n2 -' 1) div (len p1)) + 1) by A63, A65, A66, XTUPLE_0:1;
( ((n1 -' 1) div (len p1)) + 1 in dom p2 & ((n2 -' 1) div (len p1)) + 1 in dom p2 ) by A63, A53;
then A70: ((n1 -' 1) div (len p1)) + 1 = ((n2 -' 1) div (len p1)) + 1 by A48, A69, FUNCT_1:def_4;
n1 = n2
proof
A71: ( 1 <= n1 & n1 <= len q3 ) by A64, FINSEQ_1:1;
A72: ( 1 <= n2 & n2 <= len q3 ) by A64, FINSEQ_1:1;
0 < len p1 by A52, A3;
then A73: ( n1 -' 1 = ((len p1) * ((n1 -' 1) div (len p1))) + ((n1 -' 1) mod (len p1)) & n2 -' 1 = ((len p1) * ((n1 -' 1) div (len p1))) + ((n1 -' 1) mod (len p1)) ) by A68, A70, NAT_D:2;
A74: (n1 -' 1) + 1 = (n1 + 1) -' 1 by A71, NAT_D:38
.= n1 by NAT_D:34 ;
(n2 -' 1) + 1 = (n2 + 1) -' 1 by A72, NAT_D:38
.= n2 by NAT_D:34 ;
hence n1 = n2 by A73, A74; ::_thesis: verum
end;
hence x1 = x2 ; ::_thesis: verum
end;
then A75: q3 is one-to-one by FUNCT_1:def_4;
A76: rng q3 = [:Y1,Y2:]
proof
now__::_thesis:_for_z_being_set_st_z_in_[:Y1,Y2:]_holds_
z_in_rng_q3
let z be set ; ::_thesis: ( z in [:Y1,Y2:] implies z in rng q3 )
assume z in [:Y1,Y2:] ; ::_thesis: z in rng q3
then consider y1, y2 being set such that
A77: ( y1 in Y1 & y2 in Y2 & z = [y1,y2] ) by ZFMISC_1:def_2;
consider n1 being set such that
A78: ( n1 in dom p1 & y1 = p1 . n1 ) by A1, A77, FUNCT_1:def_3;
A79: n1 in Seg (len p1) by A78, FINSEQ_1:def_3;
reconsider n1 = n1 as Element of NAT by A78;
consider n2 being set such that
A80: ( n2 in dom p2 & y2 = p2 . n2 ) by A48, A77, FUNCT_1:def_3;
A81: n2 in Seg (len p2) by A80, FINSEQ_1:def_3;
reconsider n2 = n2 as Element of NAT by A80;
A82: ( 1 <= n1 & n1 <= len p1 ) by A79, FINSEQ_1:1;
A83: ( 1 <= n2 & n2 <= len p2 ) by A81, FINSEQ_1:1;
reconsider n11 = n1 - 1 as Element of NAT by A82, INT_1:5;
reconsider n21 = n2 - 1 as Element of NAT by A83, INT_1:5;
set k1 = n11 + ((len p1) * n21);
A84: n11 <= (len p1) - 1 by A82, XREAL_1:9;
(len p1) - 1 < len p1 by XREAL_1:44;
then A85: n11 < len p1 by A84, XXREAL_0:2;
A86: (n11 + ((len p1) * n21)) div (len p1) = (n11 div (len p1)) + n21 by A62, NAT_D:61
.= 0 + n21 by A85, NAT_D:27
.= n21 ;
A87: (n11 + ((len p1) * n21)) mod (len p1) = n11 mod (len p1) by NAT_D:61
.= n11 by A85, NAT_D:24 ;
set k = (n11 + ((len p1) * n21)) + 1;
A88: 1 <= (n11 + ((len p1) * n21)) + 1 by NAT_1:14;
A89: ((n11 + ((len p1) * n21)) + 1) -' 1 = ((n11 + ((len p1) * n21)) + 1) - 1 by NAT_1:14, XREAL_1:233
.= n11 + ((len p1) * n21) ;
then A90: n1 = ((((n11 + ((len p1) * n21)) + 1) -' 1) mod (len p1)) + 1 by A87;
A91: n2 = ((((n11 + ((len p1) * n21)) + 1) -' 1) div (len p1)) + 1 by A89, A86;
A92: (n11 + 1) + ((len p1) * n21) <= (len p1) + ((len p1) * n21) by A82, XREAL_1:6;
n21 <= (len p2) - 1 by A83, XREAL_1:9;
then (len p1) * n21 <= (len p1) * ((len p2) - 1) by XREAL_1:64;
then (len p1) + ((len p1) * n21) <= (len p1) + ((len p1) * ((len p2) - 1)) by XREAL_1:6;
then (n11 + ((len p1) * n21)) + 1 <= (len p1) * (len p2) by A92, XXREAL_0:2;
then (n11 + ((len p1) * n21)) + 1 in Seg (len FG) by A49, A88;
then A93: (n11 + ((len p1) * n21)) + 1 in dom FG by FINSEQ_1:def_3;
then q3 . ((n11 + ((len p1) * n21)) + 1) = z by A77, A78, A80, A50, A90, A91;
hence z in rng q3 by A93, FUNCT_1:3; ::_thesis: verum
end;
then A94: [:Y1,Y2:] c= rng q3 by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_rng_q3_holds_
z_in_[:Y1,Y2:]
let z be set ; ::_thesis: ( z in rng q3 implies z in [:Y1,Y2:] )
assume z in rng q3 ; ::_thesis: z in [:Y1,Y2:]
then consider n1 being set such that
A95: ( n1 in dom q3 & z = q3 . n1 ) by FUNCT_1:def_3;
reconsider n1 = n1 as Element of NAT by A95;
A96: z = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by A95, A50;
A97: p1 . (((n1 -' 1) mod (len p1)) + 1) in Y1 by A1, A95, A53, FUNCT_1:3;
((n1 -' 1) div (len p1)) + 1 in dom p2 by A95, A53;
then p2 . (((n1 -' 1) div (len p1)) + 1) in Y2 by A48, FUNCT_1:3;
hence z in [:Y1,Y2:] by A96, A97, ZFMISC_1:def_2; ::_thesis: verum
end;
then rng q3 c= [:Y1,Y2:] by TARSKI:def_3;
hence rng q3 = [:Y1,Y2:] by A94, XBOOLE_0:def_10; ::_thesis: verum
end;
set q30 = q3 | ((len p1) * n);
(len p1) * n <= (len p1) * (len p2) by A48, NAT_1:11, XREAL_1:64;
then A98: len (q3 | ((len p1) * n)) = (len p1) * n by A49, FINSEQ_1:17;
set q31 = q3 /^ ((len p1) * n);
reconsider q30 = q3 | ((len p1) * n) as FinSequence of [:DX1,DX2:] ;
reconsider q31 = q3 /^ ((len p1) * n) as FinSequence of [:DX1,DX2:] ;
A99: q3 = q30 ^ q31 by RFINSEQ:8;
set p20 = p2 | n;
reconsider p20 = p2 | n as FinSequence of DX2 ;
A100: len p20 = n by A48, FINSEQ_3:53;
then A101: not dom p20 is empty by A47, FINSEQ_1:def_3;
A102: p20 is one-to-one by A48, FUNCT_1:52;
reconsider Y20 = rng p20 as non empty finite Subset of DX2 by A101, RELAT_1:42;
A103: q30 is one-to-one by A75, FUNCT_1:52;
A104: rng q30 = [:Y1,Y20:]
proof
now__::_thesis:_for_z_being_set_st_z_in_[:Y1,Y20:]_holds_
z_in_rng_q30
let z be set ; ::_thesis: ( z in [:Y1,Y20:] implies z in rng q30 )
assume z in [:Y1,Y20:] ; ::_thesis: z in rng q30
then consider y1, y2 being set such that
A105: ( y1 in Y1 & y2 in Y20 & z = [y1,y2] ) by ZFMISC_1:def_2;
consider n1 being set such that
A106: ( n1 in dom p1 & y1 = p1 . n1 ) by A1, A105, FUNCT_1:def_3;
A107: n1 in Seg (len p1) by A106, FINSEQ_1:def_3;
reconsider n1 = n1 as Element of NAT by A106;
consider n2 being set such that
A108: ( n2 in dom p20 & y2 = p20 . n2 ) by A105, FUNCT_1:def_3;
A109: n2 in Seg (len p20) by A108, FINSEQ_1:def_3;
reconsider n2 = n2 as Element of NAT by A108;
A110: y2 = p2 . n2 by A108, FUNCT_1:47;
A111: ( 1 <= n1 & n1 <= len p1 ) by A107, FINSEQ_1:1;
A112: ( 1 <= n2 & n2 <= len p20 ) by A109, FINSEQ_1:1;
reconsider n11 = n1 - 1 as Element of NAT by A111, INT_1:5;
reconsider n21 = n2 - 1 as Element of NAT by A112, INT_1:5;
set k1 = n11 + ((len p1) * n21);
A113: n11 <= (len p1) - 1 by A111, XREAL_1:9;
(len p1) - 1 < len p1 by XREAL_1:44;
then A114: n11 < len p1 by A113, XXREAL_0:2;
A115: (n11 + ((len p1) * n21)) div (len p1) = (n11 div (len p1)) + n21 by A62, NAT_D:61
.= 0 + n21 by A114, NAT_D:27
.= n21 ;
A116: (n11 + ((len p1) * n21)) mod (len p1) = n11 mod (len p1) by NAT_D:61
.= n11 by A114, NAT_D:24 ;
set k = (n11 + ((len p1) * n21)) + 1;
A117: 1 <= (n11 + ((len p1) * n21)) + 1 by NAT_1:14;
A118: ((n11 + ((len p1) * n21)) + 1) -' 1 = ((n11 + ((len p1) * n21)) + 1) - 1 by NAT_1:14, XREAL_1:233
.= n11 + ((len p1) * n21) ;
then A119: n1 = ((((n11 + ((len p1) * n21)) + 1) -' 1) mod (len p1)) + 1 by A116;
A120: n2 = ((((n11 + ((len p1) * n21)) + 1) -' 1) div (len p1)) + 1 by A118, A115;
A121: (n11 + 1) + ((len p1) * n21) <= (len p1) + ((len p1) * n21) by A111, XREAL_1:6;
n21 <= (len p20) - 1 by A112, XREAL_1:9;
then (len p1) * n21 <= (len p1) * ((len p20) - 1) by XREAL_1:64;
then (len p1) + ((len p1) * n21) <= (len p1) + ((len p1) * ((len p20) - 1)) by XREAL_1:6;
then (n11 + ((len p1) * n21)) + 1 <= (len p1) * n by A121, A100, XXREAL_0:2;
then (n11 + ((len p1) * n21)) + 1 in Seg (len q30) by A117, A98;
then A122: (n11 + ((len p1) * n21)) + 1 in dom q30 by FINSEQ_1:def_3;
then A123: (n11 + ((len p1) * n21)) + 1 in dom q3 by RELAT_1:57;
q30 . ((n11 + ((len p1) * n21)) + 1) = q3 . ((n11 + ((len p1) * n21)) + 1) by A122, FUNCT_1:47
.= z by A105, A106, A110, A50, A123, A119, A120 ;
hence z in rng q30 by A122, FUNCT_1:3; ::_thesis: verum
end;
then A124: [:Y1,Y20:] c= rng q30 by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_rng_q30_holds_
z_in_[:Y1,Y20:]
let z be set ; ::_thesis: ( z in rng q30 implies z in [:Y1,Y20:] )
assume z in rng q30 ; ::_thesis: z in [:Y1,Y20:]
then consider n1 being set such that
A125: ( n1 in dom q30 & z = q30 . n1 ) by FUNCT_1:def_3;
A126: n1 in Seg (len q30) by A125, FINSEQ_1:def_3;
reconsider n1 = n1 as Element of NAT by A125;
A127: n1 in dom q3 by A125, RELAT_1:57;
z = q3 . n1 by A125, FUNCT_1:47;
then A128: z = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by A50, A127;
A129: p1 . (((n1 -' 1) mod (len p1)) + 1) in Y1 by A1, A127, A53, FUNCT_1:3;
A130: ( 1 <= n1 & n1 <= (len p1) * n ) by A126, A98, FINSEQ_1:1;
A131: len p1 divides (len p1) * n by INT_1:def_3;
A132: 1 <= len p1 by A62, NAT_1:14;
1 <= (len p1) * n by A62, A47, NAT_1:14;
then A133: (((len p1) * n) -' 1) div (len p1) = (((len p1) * n) div (len p1)) - 1 by A131, A132, NAT_2:15
.= n - 1 by A62, NAT_D:20 ;
n1 -' 1 <= ((len p1) * n) -' 1 by A130, NAT_D:42;
then (n1 -' 1) div (len p1) <= (((len p1) * n) -' 1) div (len p1) by NAT_2:24;
then A134: ((n1 -' 1) div (len p1)) + 1 <= (n - 1) + 1 by A133, XREAL_1:6;
((n1 -' 1) div (len p1)) + 1 in dom p2 by A127, A53;
then ((n1 -' 1) div (len p1)) + 1 in Seg (len p2) by FINSEQ_1:def_3;
then ( 1 <= ((n1 -' 1) div (len p1)) + 1 & ((n1 -' 1) div (len p1)) + 1 <= n ) by A134, FINSEQ_1:1;
then A135: ((n1 -' 1) div (len p1)) + 1 in Seg n ;
((n1 -' 1) div (len p1)) + 1 in dom p2 by A127, A53;
then A136: ((n1 -' 1) div (len p1)) + 1 in dom p20 by A135, RELAT_1:57;
then p20 . (((n1 -' 1) div (len p1)) + 1) in Y20 by FUNCT_1:3;
then p2 . (((n1 -' 1) div (len p1)) + 1) in Y20 by A136, FUNCT_1:47;
hence z in [:Y1,Y20:] by A128, A129, ZFMISC_1:def_2; ::_thesis: verum
end;
then rng q30 c= [:Y1,Y20:] by TARSKI:def_3;
hence rng q30 = [:Y1,Y20:] by A124, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_set_st_x_in_Y1_&_y_in_Y20_holds_
G_._(x,y)_=_(F1_._x)_*_(F2_._y)
let x, y be set ; ::_thesis: ( x in Y1 & y in Y20 implies G . (x,y) = (F1 . x) * (F2 . y) )
assume A137: ( x in Y1 & y in Y20 ) ; ::_thesis: G . (x,y) = (F1 . x) * (F2 . y)
Y20 c= rng p2 by RELAT_1:70;
hence G . (x,y) = (F1 . x) * (F2 . y) by A48, A137; ::_thesis: verum
end;
then A138: Sum (Func_Seq (G,q30)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p20))) by A46, A102, A103, A104, A100;
dom F1 = DX1 by FUNCT_2:def_1;
then A139: dom (F1 * p1) = dom p1 by A1, RELAT_1:27
.= Seg (len p1) by FINSEQ_1:def_3 ;
A140: dom G = [:DX1,DX2:] by FUNCT_2:def_1;
len q3 = (n * (len p1)) + (len p1) by A48, A49;
then A141: n * (len p1) <= len q3 by NAT_1:11;
then A142: len q31 = (len q3) - ((len p1) * n) by RFINSEQ:def_1
.= len p1 by A48, A49 ;
A143: ( [:Y1,Y2:] c= [:DX1,DX2:] & rng q31 c= rng q3 ) by A48, FINSEQ_5:33;
then A144: dom (G * q31) = dom q31 by A140, RELAT_1:27
.= Seg (len p1) by A142, FINSEQ_1:def_3 ;
then A145: dom (G * q31) = dom (((Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1)) by A139, VALUED_1:def_5;
now__::_thesis:_for_x_being_set_st_x_in_dom_(G_*_q31)_holds_
(G_*_q31)_._x_=_(((Func_Seq_(F2,p2))_/._(n_+_1))_(#)_(F1_*_p1))_._x
let x be set ; ::_thesis: ( x in dom (G * q31) implies (G * q31) . x = (((Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1)) . x )
assume A146: x in dom (G * q31) ; ::_thesis: (G * q31) . x = (((Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1)) . x
then reconsider nx = x as Element of NAT ;
A147: dom (G * q31) = dom q31 by A140, A143, RELAT_1:27
.= Seg (len q31) by FINSEQ_1:def_3 ;
A148: ( 1 <= nx & nx <= len p1 ) by A146, A144, FINSEQ_1:1;
then A149: p1 /. nx = p1 . nx by FINSEQ_4:15;
A150: ( 1 <= n + 1 & n + 1 <= len p2 ) by A48, XREAL_1:31;
then A151: n + 1 in Seg (len p2) ;
then A152: n + 1 in dom p2 by FINSEQ_1:def_3;
A153: p2 /. (n + 1) = p2 . (n + 1) by A150, FINSEQ_4:15;
dom F2 = DX2 by FUNCT_2:def_1;
then rng p2 c= dom F2 ;
then A154: n + 1 in dom (F2 * p2) by A152, RELAT_1:27;
A155: F2 . (p2 /. (n + 1)) = (F2 * p2) . (n + 1) by A152, A153, FUNCT_1:13
.= (Func_Seq (F2,p2)) /. (n + 1) by A154, PARTFUN1:def_6 ;
A156: ( 1 <= nx & nx <= len p1 ) by A147, A146, A142, FINSEQ_1:1;
then A157: nx + ((len p1) * n) <= (len p1) + ((len p1) * n) by XREAL_1:6;
A158: nx <= nx + ((len p1) * n) by NAT_1:11;
then ( 1 <= nx + ((len p1) * n) & nx + ((len p1) * n) <= (len p1) * (len p2) ) by A157, A48, A156, XXREAL_0:2;
then nx + ((len p1) * n) in dom FG by A51;
then A159: q3 . (nx + ((len p1) * n)) = [(p1 . ((((nx + ((len p1) * n)) -' 1) mod (len p1)) + 1)),(p2 . ((((nx + ((len p1) * n)) -' 1) div (len p1)) + 1))] by A50;
A160: nx in dom q31 by A147, A146, FINSEQ_1:def_3;
A161: (nx + ((len p1) * n)) -' 1 = (nx + ((len p1) * n)) - 1 by A158, A156, XREAL_1:233, XXREAL_0:2
.= (nx - 1) + ((len p1) * n)
.= (nx -' 1) + ((len p1) * n) by A148, XREAL_1:233 ;
nx - 1 < nx by XREAL_1:44;
then nx - 1 < len p1 by A156, XXREAL_0:2;
then A162: nx -' 1 < len p1 by A148, XREAL_1:233;
A163: (((nx -' 1) + ((len p1) * n)) div (len p1)) + 1 = (((nx -' 1) div (len p1)) + n) + 1 by A62, NAT_D:61
.= (0 + n) + 1 by A162, NAT_D:27 ;
A164: (((nx -' 1) + ((len p1) * n)) mod (len p1)) + 1 = ((nx -' 1) mod (len p1)) + 1 by NAT_D:61
.= (nx -' 1) + 1 by A162, NAT_D:24
.= (nx - 1) + 1 by A148, XREAL_1:233 ;
A165: ( nx in dom p1 & n + 1 in dom p2 ) by A146, A144, A151, FINSEQ_1:def_3;
then ( p1 /. nx = p1 . nx & p2 . (n + 1) = p2 /. (n + 1) ) by PARTFUN1:def_6;
then A166: q31 . nx = [(p1 /. nx),(p2 /. (n + 1))] by A160, A159, A141, A161, A163, A164, RFINSEQ:def_1;
( p1 . nx in Y1 & p2 . (n + 1) in Y2 ) by A165, A48, A1, FUNCT_1:3;
then A167: ( p1 /. nx in Y1 & p2 /. (n + 1) in Y2 ) by A165, PARTFUN1:def_6;
thus (G * q31) . x = G . ((p1 /. nx),(p2 /. (n + 1))) by A166, A146, FUNCT_1:12
.= (F1 . (p1 /. nx)) * (F2 . (p2 /. (n + 1))) by A48, A167
.= ((F1 * p1) . nx) * ((Func_Seq (F2,p2)) /. (n + 1)) by A155, A149, A139, A146, A144, FUNCT_1:12
.= (((Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1)) . x by VALUED_1:6 ; ::_thesis: verum
end;
then Func_Seq (G,q31) = ((Func_Seq (F2,p2)) /. (n + 1)) * (Func_Seq (F1,p1)) by A145, FUNCT_1:2;
then A168: Sum (Func_Seq (G,q31)) = (Sum (Func_Seq (F1,p1))) * ((Func_Seq (F2,p2)) /. (n + 1)) by RVSUM_1:87;
A169: Func_Seq (G,q3) = (Func_Seq (G,q30)) ^ (Func_Seq (G,q31)) by A99, Lm5;
dom F2 = DX2 by FUNCT_2:def_1;
then rng p2 c= dom F2 ;
then dom (F2 * p2) = dom p2 by RELAT_1:27;
then dom (Func_Seq (F2,p2)) = Seg (len p2) by FINSEQ_1:def_3;
then A170: len (Func_Seq (F2,p2)) = n + 1 by A48, FINSEQ_1:def_3;
(Func_Seq (F2,p2)) | n = Func_Seq (F2,p20) by RELAT_1:83;
then A171: Func_Seq (F2,p2) = (Func_Seq (F2,p20)) ^ <*((Func_Seq (F2,p2)) /. (n + 1))*> by A170, FINSEQ_5:21;
A172: Sum (Func_Seq (G,q3)) = (Sum (Func_Seq (G,q30))) + (Sum (Func_Seq (G,q31))) by A169, RVSUM_1:75
.= (Sum (Func_Seq (F1,p1))) * ((Sum (Func_Seq (F2,p20))) + ((Func_Seq (F2,p2)) /. (n + 1))) by A138, A168
.= (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A171, RVSUM_1:74 ;
consider P being Permutation of (dom p3) such that
A173: ( q3 = p3 * P & dom P = dom p3 & rng P = dom p3 ) by A75, A76, A48, BHSP_5:1;
A174: Func_Seq (G,q3) = (Func_Seq (G,p3)) * P by A173, RELAT_1:36;
dom G = [:DX1,DX2:] by FUNCT_2:def_1;
then rng p3 c= dom G ;
then dom (Func_Seq (G,p3)) = dom p3 by RELAT_1:27;
hence Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A172, A174, FINSOP_1:7; ::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
A175: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A45);
now__::_thesis:_for_p2_being_FinSequence_of_DX2
for_p3_being_FinSequence_of_[:DX1,DX2:]
for_Y2_being_non_empty_finite_Subset_of_DX2
for_Y3_being_finite_Subset_of_[:DX1,DX2:]_st_p2_is_one-to-one_&_rng_p2_=_Y2_&_p3_is_one-to-one_&_rng_p3_=_Y3_&_Y3_=_[:Y1,Y2:]_&_(_for_x,_y_being_set_st_x_in_Y1_&_y_in_Y2_holds_
G_._(x,y)_=_(F1_._x)_*_(F2_._y)_)_holds_
Sum_(Func_Seq_(G,p3))_=_(Sum_(Func_Seq_(F1,p1)))_*_(Sum_(Func_Seq_(F2,p2)))
let p2 be FinSequence of DX2; ::_thesis: for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let p3 be FinSequence of [:DX1,DX2:]; ::_thesis: for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y2 be non empty finite Subset of DX2; ::_thesis: for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
let Y3 be finite Subset of [:DX1,DX2:]; ::_thesis: ( p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) implies Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) )
assume A176: ( p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) ) ; ::_thesis: Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
len p2 is Element of NAT ;
hence Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A175, A176; ::_thesis: verum
end;
hence for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) ; ::_thesis: verum
end;
theorem Th12: :: RANDOM_2:12
for DX1, DX2 being non empty set
for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
proof
let DX1, DX2 be non empty set ; ::_thesis: for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
let F1 be Function of DX1,REAL; ::_thesis: for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
let F2 be Function of DX2,REAL; ::_thesis: for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
let G be Function of [:DX1,DX2:],REAL; ::_thesis: for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
let Y1 be non empty finite Subset of DX1; ::_thesis: for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
let Y2 be non empty finite Subset of DX2; ::_thesis: for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
let Y3 be finite Subset of [:DX1,DX2:]; ::_thesis: ( Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) implies setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal)) )
assume A1: ( Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) ) ; ::_thesis: setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
consider p1 being FinSequence of DX1 such that
A2: ( p1 is one-to-one & rng p1 = Y1 & setopfunc (Y1,DX1,REAL,F1,addreal) = Sum (Func_Seq (F1,p1)) ) by Th9;
consider p2 being FinSequence of DX2 such that
A3: ( p2 is one-to-one & rng p2 = Y2 & setopfunc (Y2,DX2,REAL,F2,addreal) = Sum (Func_Seq (F2,p2)) ) by Th9;
consider p3 being FinSequence of [:DX1,DX2:] such that
A4: ( p3 is one-to-one & rng p3 = Y3 & setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = Sum (Func_Seq (G,p3)) ) by Th9;
thus setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal)) by A1, A2, A3, A4, Th11; ::_thesis: verum
end;
theorem Th13: :: RANDOM_2:13
for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX st ( for x being set st x in Y holds
0 <= F . x ) holds
0 <= setopfunc (Y,DX,REAL,F,addreal)
proof
let DX be non empty set ; ::_thesis: for F being Function of DX,REAL
for Y being finite Subset of DX st ( for x being set st x in Y holds
0 <= F . x ) holds
0 <= setopfunc (Y,DX,REAL,F,addreal)
let F be Function of DX,REAL; ::_thesis: for Y being finite Subset of DX st ( for x being set st x in Y holds
0 <= F . x ) holds
0 <= setopfunc (Y,DX,REAL,F,addreal)
let Y be finite Subset of DX; ::_thesis: ( ( for x being set st x in Y holds
0 <= F . x ) implies 0 <= setopfunc (Y,DX,REAL,F,addreal) )
assume A1: for x being set st x in Y holds
0 <= F . x ; ::_thesis: 0 <= setopfunc (Y,DX,REAL,F,addreal)
consider p being FinSequence of DX such that
A2: ( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) ) by Th9;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Func_Seq_(F,p))_holds_
0_<=_(Func_Seq_(F,p))_._i
let i be Nat; ::_thesis: ( i in dom (Func_Seq (F,p)) implies 0 <= (Func_Seq (F,p)) . i )
assume A3: i in dom (Func_Seq (F,p)) ; ::_thesis: 0 <= (Func_Seq (F,p)) . i
then A4: (Func_Seq (F,p)) . i = F . (p . i) by FUNCT_1:12;
i in dom p by A3, FUNCT_1:11;
hence 0 <= (Func_Seq (F,p)) . i by A4, A1, A2, FUNCT_1:3; ::_thesis: verum
end;
hence 0 <= setopfunc (Y,DX,REAL,F,addreal) by A2, RVSUM_1:84; ::_thesis: verum
end;
theorem Th14: :: RANDOM_2:14
for DX being non empty set
for F being Function of DX,REAL
for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) holds
setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
proof
let DX be non empty set ; ::_thesis: for F being Function of DX,REAL
for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) holds
setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
let F be Function of DX,REAL; ::_thesis: for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) holds
setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
let Y1, Y2 be finite Subset of DX; ::_thesis: ( Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) implies setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal) )
assume A1: ( Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) ) ; ::_thesis: setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
consider p1 being FinSequence of DX such that
A2: ( p1 is one-to-one & rng p1 = Y1 & setopfunc (Y1,DX,REAL,F,addreal) = Sum (Func_Seq (F,p1)) ) by Th9;
reconsider Y3 = Y2 \ Y1 as finite Subset of DX ;
consider p2 being FinSequence of DX such that
A3: ( p2 is one-to-one & rng p2 = Y3 & setopfunc (Y3,DX,REAL,F,addreal) = Sum (Func_Seq (F,p2)) ) by Th9;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Func_Seq_(F,p2))_holds_
0_<=_(Func_Seq_(F,p2))_._i
let i be Nat; ::_thesis: ( i in dom (Func_Seq (F,p2)) implies 0 <= (Func_Seq (F,p2)) . i )
assume A4: i in dom (Func_Seq (F,p2)) ; ::_thesis: 0 <= (Func_Seq (F,p2)) . i
then A5: (Func_Seq (F,p2)) . i = F . (p2 . i) by FUNCT_1:12;
i in dom p2 by A4, FUNCT_1:11;
then A6: p2 . i in Y3 by A3, FUNCT_1:3;
Y3 c= Y2 by XBOOLE_1:36;
hence 0 <= (Func_Seq (F,p2)) . i by A5, A1, A6; ::_thesis: verum
end;
then A7: 0 <= Sum (Func_Seq (F,p2)) by RVSUM_1:84;
reconsider p3 = p1 ^ p2 as FinSequence of DX ;
A8: rng p3 = (rng p1) \/ (rng p2) by FINSEQ_1:31
.= Y1 \/ Y2 by A3, A2, XBOOLE_1:39
.= Y2 by A1, XBOOLE_1:12 ;
rng p1 misses rng p2 by A2, A3, XBOOLE_1:79;
then p3 is one-to-one by A2, A3, FINSEQ_3:91;
then A9: setopfunc (Y2,DX,REAL,F,addreal) = Sum (Func_Seq (F,p3)) by A8, Th10;
A10: Func_Seq (F,p3) = (Func_Seq (F,p1)) ^ (Func_Seq (F,p2)) by Lm5;
(Sum (Func_Seq (F,p1))) + 0 <= (Sum (Func_Seq (F,p1))) + (Sum (Func_Seq (F,p2))) by A7, XREAL_1:6;
hence setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal) by A2, A10, A9, RVSUM_1:75; ::_thesis: verum
end;
theorem Th15: :: RANDOM_2:15
for Omega being non empty finite set
for P being Probability of Trivial-SigmaField Omega
for Y being non empty finite Subset of Omega
for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )
proof
let Omega be non empty finite set ; ::_thesis: for P being Probability of Trivial-SigmaField Omega
for Y being non empty finite Subset of Omega
for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )
let P be Probability of Trivial-SigmaField Omega; ::_thesis: for Y being non empty finite Subset of Omega
for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )
let Y be non empty finite Subset of Omega; ::_thesis: for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )
let f be Function of Omega,REAL; ::_thesis: ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )
set YN = Omega \ Y;
A1: ( dom ((Omega \ Y) --> 0) = Omega \ Y & rng ((Omega \ Y) --> 0) c= REAL ) by FUNCOP_1:13;
A2: dom (f +* ((Omega \ Y) --> 0)) = (dom f) \/ (dom ((Omega \ Y) --> 0)) by FUNCT_4:def_1
.= Omega \/ (Omega \ Y) by A1, FUNCT_2:def_1
.= Omega by XBOOLE_1:12 ;
rng (f +* ((Omega \ Y) --> 0)) c= REAL ;
then reconsider g = f +* ((Omega \ Y) --> 0) as Function of Omega,REAL by A2, FUNCT_2:2;
consider G being FinSequence of REAL , s being FinSequence of Omega such that
A3: ( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds
G . n = (g . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),g) = Sum G ) by RANDOM_1:13;
reconsider g = g as Real-Valued-Random-Variable of Trivial-SigmaField Omega by RANDOM_1:29;
A4: dom g = Omega by FUNCT_2:def_1;
g is_integrable_on P by RANDOM_1:30;
then A5: g is_integrable_on P2M P by RANDOM_1:def_3;
A6: Y misses Omega \ Y by XBOOLE_1:79;
A7: Integral ((P2M P),(g | (Y \/ (Omega \ Y)))) = (Integral ((P2M P),(g | Y))) + (Integral ((P2M P),(g | (Omega \ Y)))) by A5, MESFUNC6:92, XBOOLE_1:79;
Y \/ (Omega \ Y) = Y \/ Omega by XBOOLE_1:39
.= Omega by XBOOLE_1:12 ;
then A8: g | (Y \/ (Omega \ Y)) = g by FUNCT_2:33;
A9: g | Y = f | Y by A1, A6, FUNCT_4:72;
A10: dom (g | (Omega \ Y)) = Omega \ Y by A4, RELAT_1:62;
A11: for x being set st x in dom (g | (Omega \ Y)) holds
(g | (Omega \ Y)) . x = 0
proof
let x be set ; ::_thesis: ( x in dom (g | (Omega \ Y)) implies (g | (Omega \ Y)) . x = 0 )
assume A12: x in dom (g | (Omega \ Y)) ; ::_thesis: (g | (Omega \ Y)) . x = 0
then A13: ( x in Omega \ Y & (g | (Omega \ Y)) . x = g . x ) by A4, FUNCT_1:47, RELAT_1:62;
g . x = ((Omega \ Y) --> 0) . x by A12, A1, A10, FUNCT_4:13;
hence (g | (Omega \ Y)) . x = 0 by A13, FUNCOP_1:7; ::_thesis: verum
end;
then Integral ((P2M P),(g | (Omega \ Y))) = (R_EAL 0) * ((P2M P) . (Omega \ Y)) by A10, MESFUNC6:97
.= R_EAL 0 ;
then A14: Integral ((P2M P),g) = Integral ((P2M P),(f | Y)) by A9, A7, A8, XXREAL_3:4;
set N1 = s " Y;
s is Function of (dom s),(rng s) by FUNCT_2:1;
then s " Y is finite Subset of (dom s) by FUNCT_2:39;
then reconsider N1 = s " Y as finite Subset of (Seg (len G)) by A3, FINSEQ_1:def_3;
rng (canFS N1) c= N1 by FINSEQ_1:def_4;
then rng (canFS N1) c= Seg (len G) by XBOOLE_1:1;
then A15: canFS N1 is FinSequence of Seg (len G) by FINSEQ_1:def_4;
dom s = Seg (len G) by A3, FINSEQ_1:def_3;
then A16: s is Function of (Seg (len G)),Omega by A3, FUNCT_2:1;
then reconsider t1 = s * (canFS N1) as FinSequence of Omega by A15, FINSEQ_2:32;
A17: rng t1 = s .: (rng (canFS N1)) by RELAT_1:127
.= s .: N1 by FUNCT_2:def_3
.= Y by A3, FUNCT_1:77 ;
set N2 = (Seg (len G)) \ N1;
reconsider N2 = (Seg (len G)) \ N1 as finite Subset of (Seg (len G)) by XBOOLE_1:36;
rng (canFS N2) c= N2 by FINSEQ_1:def_4;
then rng (canFS N2) c= Seg (len G) by XBOOLE_1:1;
then canFS N2 is FinSequence of Seg (len G) by FINSEQ_1:def_4;
then reconsider t2 = s * (canFS N2) as FinSequence of Omega by A16, FINSEQ_2:32;
reconsider t = t1 ^ t2 as FinSequence of Omega ;
A18: rng (canFS N1) = N1 by FUNCT_2:def_3;
A19: rng (canFS N2) = N2 by FUNCT_2:def_3;
A20: ( N1 is finite Subset of (dom s) & N2 is finite Subset of (dom s) ) by A3, FINSEQ_1:def_3;
then rng (s | N1) misses rng (s | N2) by Th1, A3, XBOOLE_1:79;
then rng t1 misses rng (s | N2) by A18, Th2, XBOOLE_1:63;
then A21: rng t1 misses rng t2 by A19, Th2, XBOOLE_1:63;
then A22: t is one-to-one by A3, FINSEQ_3:91;
len (canFS N1) = card N1 by UPROOTS:3;
then A23: dom (canFS N1) = Seg (card N1) by FINSEQ_1:def_3;
rng (canFS N1) is Subset of (dom s) by A20, FUNCT_2:def_3;
then dom t1 = Seg (card N1) by A23, RELAT_1:27;
then A24: len t1 = card N1 by FINSEQ_1:def_3;
len (canFS N2) = card N2 by UPROOTS:3;
then A25: dom (canFS N2) = Seg (card N2) by FINSEQ_1:def_3;
rng (canFS N2) is Subset of (dom s) by A20, FUNCT_2:def_3;
then dom t2 = Seg (card N2) by A25, RELAT_1:27;
then A26: len t2 = card N2 by FINSEQ_1:def_3;
A27: N1 \/ N2 = (Seg (len G)) \/ N1 by XBOOLE_1:39
.= Seg (len G) by XBOOLE_1:12
.= dom s by A3, FINSEQ_1:def_3 ;
dom t = Seg ((len t1) + (len t2)) by FINSEQ_1:def_7
.= Seg (card (N1 \/ N2)) by A24, A26, CARD_2:40, XBOOLE_1:79 ;
then A28: len t = card (N1 \/ N2) by FINSEQ_1:def_3;
then A29: len t = len s by A27, CARD_1:62;
A30: Seg (len s) = Seg (len t) by A28, A27, CARD_1:62;
A31: dom s = Seg (len s) by FINSEQ_1:def_3
.= dom t by A30, FINSEQ_1:def_3 ;
A32: card (dom t) = card Omega by A3, A29, CARD_1:62;
t is Function of (dom t),Omega by FINSEQ_2:26;
then rng s = rng t by A3, A22, A32, FINSEQ_4:63;
then consider PN being Permutation of (dom s) such that
A33: ( t = s * PN & dom PN = dom s & rng PN = dom s ) by A3, A22, BHSP_5:1;
defpred S1[ set , set ] means ( ( t . $1 in Y implies $2 = (f . (t . $1)) * (P . {(t . $1)}) ) & ( not t . $1 in Y implies $2 = (g . (t . $1)) * (P . {(t . $1)}) ) );
A34: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(card_Omega)_holds_
ex_x_being_Element_of_REAL_st_S1[k,x]
let k be Nat; ::_thesis: ( k in Seg (card Omega) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (card Omega) ; ::_thesis: ex x being Element of REAL st S1[k,x]
now__::_thesis:_ex_x_being_Element_of_REAL_st_S1[k,x]
percases ( t . k in Y or not t . k in Y ) ;
suppose t . k in Y ; ::_thesis: ex x being Element of REAL st S1[k,x]
hence ex x being Element of REAL st S1[k,x] ; ::_thesis: verum
end;
suppose not t . k in Y ; ::_thesis: ex x being Element of REAL st S1[k,x]
hence ex x being Element of REAL st S1[k,x] ; ::_thesis: verum
end;
end;
end;
hence ex x being Element of REAL st S1[k,x] ; ::_thesis: verum
end;
consider F being FinSequence of REAL such that
A35: dom F = Seg (card Omega) and
A36: for n being Nat st n in Seg (card Omega) holds
S1[n,F . n] from FINSEQ_1:sch_5(A34);
A37: dom s = Seg (len G) by A3, FINSEQ_1:def_3
.= dom G by FINSEQ_1:def_3 ;
then A38: dom (G * PN) = dom PN by A33, RELAT_1:27;
A39: dom F = dom s by A3, A35, FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
F_._x_=_(G_*_PN)_._x
let x be set ; ::_thesis: ( x in dom F implies F . x = (G * PN) . x )
assume A40: x in dom F ; ::_thesis: F . x = (G * PN) . x
then reconsider nx = x as Element of NAT ;
A41: nx in dom t by A40, A3, A35, A31, FINSEQ_1:def_3;
A42: t . nx = s . (PN . nx) by A33, A40, A39, A31, FUNCT_1:12;
PN . nx in dom G by A37, A41, A33, FUNCT_1:11;
then A43: G . (PN . nx) = (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A3;
now__::_thesis:_F_._nx_=_(G_*_PN)_._nx
percases ( t . nx in Y or not t . nx in Y ) ;
supposeA44: t . nx in Y ; ::_thesis: F . nx = (G * PN) . nx
hence F . nx = (f . (t . nx)) * (P . {(t . nx)}) by A36, A35, A40
.= ((f | Y) . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A42, A44, FUNCT_1:49
.= (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A44, A42, A9, FUNCT_1:49
.= (G * PN) . nx by A39, A40, A33, A43, FUNCT_1:13 ;
::_thesis: verum
end;
suppose not t . nx in Y ; ::_thesis: F . nx = (G * PN) . nx
hence F . nx = (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A42, A36, A35, A40
.= (G * PN) . nx by A39, A40, A33, A43, FUNCT_1:13 ;
::_thesis: verum
end;
end;
end;
hence F . x = (G * PN) . x ; ::_thesis: verum
end;
then F = G * PN by A33, A38, A39, FUNCT_1:2;
then A45: Sum G = Sum F by A37, FINSOP_1:7;
reconsider t1 = t1 as FinSequence of Y by A17, FINSEQ_1:def_4;
reconsider F1 = F | (len t1) as FinSequence of REAL ;
reconsider F2 = F /^ (len t1) as FinSequence of REAL ;
A46: F = F1 ^ F2 by RFINSEQ:8;
A47: len t1 = card Y by A17, A3, FINSEQ_4:62;
A48: len F = card Omega by A35, FINSEQ_1:def_3;
A49: len F = len t by A29, A3, A35, FINSEQ_1:def_3;
A50: len t = (len t1) + (len t2) by FINSEQ_1:22;
then A51: len t1 <= len t by NAT_1:11;
then A52: len F2 = (len F) - (len t1) by A49, RFINSEQ:def_1
.= len t2 by A50, A49 ;
then A53: dom F2 = Seg (len t2) by FINSEQ_1:def_3
.= dom ((len t2) |-> 0) by FUNCOP_1:13 ;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_F2_holds_
F2_._m_=_((len_t2)_|->_0)_._m
let m be Nat; ::_thesis: ( m in dom F2 implies F2 . m = ((len t2) |-> 0) . m )
assume A54: m in dom F2 ; ::_thesis: F2 . m = ((len t2) |-> 0) . m
then A55: m in Seg (len t2) by A52, FINSEQ_1:def_3;
then A56: m in dom t2 by FINSEQ_1:def_3;
A57: ( 1 <= m & m <= len t2 ) by A55, FINSEQ_1:1;
m <= m + (len t1) by NAT_1:11;
then ( 1 <= m + (len t1) & m + (len t1) <= len t ) by A50, A57, XREAL_1:6, XXREAL_0:2;
then A58: m + (len t1) in Seg (card Omega) by A3, A29;
A59: t . (m + (len t1)) = t2 . m by A56, FINSEQ_1:def_7;
A60: (rng t1) /\ (rng t2) = {} by A21, XBOOLE_0:def_7;
A61: t2 . m in rng t2 by A56, FUNCT_1:3;
then not t2 . m in rng t1 by A60, XBOOLE_0:def_4;
then A62: t2 . m in dom (g | (Omega \ Y)) by A10, A17, A61, XBOOLE_0:def_5;
then A63: g . (t2 . m) = (g | (Omega \ Y)) . (t2 . m) by FUNCT_1:47
.= 0 by A11, A62 ;
not t . (m + (len t1)) in Y by A17, A60, A61, A59, XBOOLE_0:def_4;
then A64: F . (m + (len t1)) = (g . (t . (m + (len t1)))) * (P . {(t . (m + (len t1)))}) by A36, A58
.= 0 by A63, A59 ;
thus F2 . m = F . (m + (len t1)) by A49, A51, A54, RFINSEQ:def_1
.= ((len t2) |-> 0) . m by A55, A64, FINSEQ_2:57 ; ::_thesis: verum
end;
then A65: F2 = (len t2) |-> 0 by A53, FINSEQ_1:13;
card Y c= card Omega by CARD_1:11;
then A66: card Y <= card Omega by NAT_1:39;
A67: Sum F = (Sum F1) + (Sum F2) by A46, RVSUM_1:75
.= (Sum F1) + 0 by A65, RVSUM_1:81
.= Sum F1 ;
A68: len F1 = card Y by A48, A47, A66, FINSEQ_1:59;
for n being Nat st n in dom F1 holds
F1 . n = (f . (t1 . n)) * (P . {(t1 . n)})
proof
let n be Nat; ::_thesis: ( n in dom F1 implies F1 . n = (f . (t1 . n)) * (P . {(t1 . n)}) )
assume n in dom F1 ; ::_thesis: F1 . n = (f . (t1 . n)) * (P . {(t1 . n)})
then A69: n in Seg (len t1) by A68, A47, FINSEQ_1:def_3;
then A70: n in dom t1 by FINSEQ_1:def_3;
then A71: t . n = t1 . n by FINSEQ_1:def_7;
then A72: t . n in Y by A17, A70, FUNCT_1:3;
A73: Seg (len t1) c= Seg (card Omega) by A47, A66, FINSEQ_1:5;
thus F1 . n = F . n by A69, FUNCT_1:49
.= (f . (t1 . n)) * (P . {(t1 . n)}) by A71, A73, A69, A36, A72 ; ::_thesis: verum
end;
hence ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G ) by A68, A47, A17, A67, A45, A3, A14; ::_thesis: verum
end;
Lm7: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Q be Function of [:Omega1,Omega2:],REAL; ::_thesis: for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let P be Function of (bool [:Omega1,Omega2:]),REAL; ::_thesis: for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y1 be non empty finite Subset of Omega1; ::_thesis: for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y2 be non empty finite Subset of Omega2; ::_thesis: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) implies P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2) )
assume A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) ; ::_thesis: P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
deffunc H1( set ) -> Element of REAL = P1 . {$1};
A2: for x being set st x in Y1 holds
H1(x) in REAL ;
consider F1 being Function of Y1,REAL such that
A3: for x being set st x in Y1 holds
F1 . x = H1(x) from FUNCT_2:sch_2(A2);
deffunc H2( set ) -> Element of REAL = P2 . {$1};
A4: for x being set st x in Y2 holds
H2(x) in REAL ;
consider F2 being Function of Y2,REAL such that
A5: for x being set st x in Y2 holds
F2 . x = H2(x) from FUNCT_2:sch_2(A4);
now__::_thesis:_for_x_being_set_st_x_in_{{},1}_holds_
x_in_REAL
let x be set ; ::_thesis: ( x in {{},1} implies x in REAL )
assume x in {{},1} ; ::_thesis: x in REAL
then ( x = 0 or x = 1 ) by TARSKI:def_2;
hence x in REAL ; ::_thesis: verum
end;
then A6: {{},1} c= REAL by TARSKI:def_3;
A7: ( dom (chi (Y1,Omega1)) = Omega1 & rng (chi (Y1,Omega1)) c= {{},1} ) by FUNCT_3:39, FUNCT_3:def_3;
then chi (Y1,Omega1) is Function of Omega1,{{},1} by FUNCT_2:def_1, RELSET_1:4;
then reconsider f1 = chi (Y1,Omega1) as Function of Omega1,REAL by A6, FUNCT_2:7;
A8: dom (f1 | Y1) = (dom f1) /\ Y1 by RELAT_1:61
.= Y1 by A7, XBOOLE_1:28 ;
for x being set st x in dom (f1 | Y1) holds
(f1 | Y1) . x = 1
proof
let x be set ; ::_thesis: ( x in dom (f1 | Y1) implies (f1 | Y1) . x = 1 )
assume A9: x in dom (f1 | Y1) ; ::_thesis: (f1 | Y1) . x = 1
then (f1 | Y1) . x = f1 . x by FUNCT_1:47
.= 1 by A9, A8, FUNCT_3:def_3 ;
hence (f1 | Y1) . x = 1 ; ::_thesis: verum
end;
then A10: Integral ((P2M P1),(f1 | Y1)) = (R_EAL 1) * ((P2M P1) . (dom (f1 | Y1))) by MESFUNC6:97
.= 1 * (P1 . Y1) by A8, EXTREAL1:1
.= P1 . Y1 ;
consider G1 being FinSequence of REAL , s1 being FinSequence of Y1 such that
A11: ( len G1 = card Y1 & s1 is one-to-one & rng s1 = Y1 & len s1 = card Y1 & ( for n being Nat st n in dom G1 holds
G1 . n = (f1 . (s1 . n)) * (P1 . {(s1 . n)}) ) & Integral ((P2M P1),(f1 | Y1)) = Sum G1 ) by Th15;
Y1 c= Y1 ;
then reconsider YY1 = Y1 as finite Subset of Y1 ;
dom F1 = Y1 by FUNCT_2:def_1;
then A12: dom (F1 * s1) = dom s1 by A11, RELAT_1:27;
A13: dom G1 = Seg (len s1) by A11, FINSEQ_1:def_3
.= dom s1 by FINSEQ_1:def_3 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_G1_holds_
G1_._x_=_(F1_*_s1)_._x
let x be set ; ::_thesis: ( x in dom G1 implies G1 . x = (F1 * s1) . x )
assume A14: x in dom G1 ; ::_thesis: G1 . x = (F1 * s1) . x
then reconsider nx = x as Element of NAT ;
A15: s1 . nx in Y1 by A11, A13, A14, FUNCT_1:3;
thus G1 . x = (f1 . (s1 . nx)) * (P1 . {(s1 . nx)}) by A11, A14
.= 1 * (P1 . {(s1 . nx)}) by A15, FUNCT_3:def_3
.= F1 . (s1 . nx) by A3, A11, A13, A14, FUNCT_1:3
.= (F1 * s1) . x by A13, A14, FUNCT_1:13 ; ::_thesis: verum
end;
then G1 = Func_Seq (F1,s1) by A12, A13, FUNCT_1:2;
then A16: setopfunc (YY1,Y1,REAL,F1,addreal) = Sum G1 by A11, Th10;
A17: ( dom (chi (Y2,Omega2)) = Omega2 & rng (chi (Y2,Omega2)) c= {{},1} ) by FUNCT_3:39, FUNCT_3:def_3;
then chi (Y2,Omega2) is Function of Omega2,{{},1} by FUNCT_2:def_1, RELSET_1:4;
then reconsider f2 = chi (Y2,Omega2) as Function of Omega2,REAL by A6, FUNCT_2:7;
A18: dom (f2 | Y2) = (dom f2) /\ Y2 by RELAT_1:61
.= Y2 by A17, XBOOLE_1:28 ;
for x being set st x in dom (f2 | Y2) holds
(f2 | Y2) . x = 1
proof
let x be set ; ::_thesis: ( x in dom (f2 | Y2) implies (f2 | Y2) . x = 1 )
assume A19: x in dom (f2 | Y2) ; ::_thesis: (f2 | Y2) . x = 1
then (f2 | Y2) . x = f2 . x by FUNCT_1:47
.= 1 by A19, A18, FUNCT_3:def_3 ;
hence (f2 | Y2) . x = 1 ; ::_thesis: verum
end;
then A20: Integral ((P2M P2),(f2 | Y2)) = (R_EAL 1) * ((P2M P2) . Y2) by A18, MESFUNC6:97
.= 1 * (P2 . Y2) by EXTREAL1:1
.= P2 . Y2 ;
consider G2 being FinSequence of REAL , s2 being FinSequence of Y2 such that
A21: ( len G2 = card Y2 & s2 is one-to-one & rng s2 = Y2 & len s2 = card Y2 & ( for n being Nat st n in dom G2 holds
G2 . n = (f2 . (s2 . n)) * (P2 . {(s2 . n)}) ) & Integral ((P2M P2),(f2 | Y2)) = Sum G2 ) by Th15;
Y2 c= Y2 ;
then reconsider YY2 = Y2 as finite Subset of Y2 ;
dom F2 = Y2 by FUNCT_2:def_1;
then A22: dom (F2 * s2) = dom s2 by A21, RELAT_1:27;
A23: dom G2 = Seg (len s2) by A21, FINSEQ_1:def_3
.= dom s2 by FINSEQ_1:def_3 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_G2_holds_
G2_._x_=_(F2_*_s2)_._x
let x be set ; ::_thesis: ( x in dom G2 implies G2 . x = (F2 * s2) . x )
assume A24: x in dom G2 ; ::_thesis: G2 . x = (F2 * s2) . x
then reconsider nx = x as Element of NAT ;
A25: s2 . nx in Y2 by A21, A23, A24, FUNCT_1:3;
thus G2 . x = (f2 . (s2 . nx)) * (P2 . {(s2 . nx)}) by A21, A24
.= 1 * (P2 . {(s2 . nx)}) by A25, FUNCT_3:def_3
.= F2 . (s2 . nx) by A5, A21, A23, A24, FUNCT_1:3
.= (F2 * s2) . x by A23, A24, FUNCT_1:13 ; ::_thesis: verum
end;
then G2 = Func_Seq (F2,s2) by A22, A23, FUNCT_1:2;
then A26: setopfunc (YY2,Y2,REAL,F2,addreal) = Sum G2 by A21, Th10;
reconsider Y3 = [:Y1,Y2:] as finite Subset of [:Y1,Y2:] by ZFMISC_1:96;
reconsider Y33 = [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:] by ZFMISC_1:96;
A27: [:Y1,Y2:] c= [:Omega1,Omega2:] by ZFMISC_1:96;
then reconsider Q0 = Q | [:Y1,Y2:] as Function of [:Y1,Y2:],REAL by FUNCT_2:32;
A28: now__::_thesis:_for_x,_y_being_set_st_x_in_Y1_&_y_in_Y2_holds_
Q0_._(x,y)_=_(F1_._x)_*_(F2_._y)
let x, y be set ; ::_thesis: ( x in Y1 & y in Y2 implies Q0 . (x,y) = (F1 . x) * (F2 . y) )
assume A29: ( x in Y1 & y in Y2 ) ; ::_thesis: Q0 . (x,y) = (F1 . x) * (F2 . y)
then [x,y] in [:Y1,Y2:] by ZFMISC_1:def_2;
then [x,y] in dom Q0 by FUNCT_2:def_1;
hence Q0 . (x,y) = Q . (x,y) by FUNCT_1:47
.= (P1 . {x}) * (P2 . {y}) by A1, A29
.= (F1 . x) * (P2 . {y}) by A29, A3
.= (F1 . x) * (F2 . y) by A29, A5 ;
::_thesis: verum
end;
Y3 c= dom Q0 by FUNCT_2:def_1;
then consider pp1 being FinSequence of [:Y1,Y2:] such that
A30: ( pp1 is one-to-one & rng pp1 = Y3 & setopfunc (Y3,[:Y1,Y2:],REAL,Q0,addreal) = addreal "**" (Func_Seq (Q0,pp1)) ) by BHSP_5:def_5;
A31: rng pp1 c= [:Omega1,Omega2:] by A27, XBOOLE_1:1;
then reconsider pp2 = pp1 as FinSequence of [:Omega1,Omega2:] by FINSEQ_1:def_4;
rng pp1 c= dom Q by A31, FUNCT_2:def_1;
then A32: dom (Q * pp1) = dom pp1 by RELAT_1:27;
A33: dom Q0 = [:Y1,Y2:] by FUNCT_2:def_1;
for x being set st x in dom (Q0 * pp1) holds
(Q0 * pp1) . x = (Q * pp1) . x
proof
let x be set ; ::_thesis: ( x in dom (Q0 * pp1) implies (Q0 * pp1) . x = (Q * pp1) . x )
assume x in dom (Q0 * pp1) ; ::_thesis: (Q0 * pp1) . x = (Q * pp1) . x
then A34: ( (Q0 * pp1) . x = Q0 . (pp1 . x) & x in dom pp1 ) by FUNCT_1:11, FUNCT_1:12;
then pp1 . x in rng pp1 by FUNCT_1:3;
then Q0 . (pp1 . x) = Q . (pp1 . x) by FUNCT_1:49;
hence (Q0 * pp1) . x = (Q * pp1) . x by A34, FUNCT_1:13; ::_thesis: verum
end;
then A35: Func_Seq (Q0,pp1) = Func_Seq (Q,pp2) by A33, A32, A31, FUNCT_1:2, RELAT_1:27;
dom Q = [:Omega1,Omega2:] by FUNCT_2:def_1;
then A36: setopfunc (Y3,[:Y1,Y2:],REAL,Q0,addreal) = setopfunc (Y33,[:Omega1,Omega2:],REAL,Q,addreal) by A30, A35, BHSP_5:def_5;
thus P . [:Y1,Y2:] = setopfunc (Y33,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= (P1 . Y1) * (P2 . Y2) by A20, A21, A10, A11, A26, A16, Th12, A28, A36 ; ::_thesis: verum
end;
Lm8: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let Q be Function of [:Omega1,Omega2:],REAL; ::_thesis: for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
let P be Function of (bool [:Omega1,Omega2:]),REAL; ::_thesis: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) implies P . [:Omega1,Omega2:] = 1 )
assume A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) ; ::_thesis: P . [:Omega1,Omega2:] = 1
deffunc H1( set ) -> Element of REAL = P1 . {$1};
A2: for x being set st x in Omega1 holds
H1(x) in REAL ;
consider F1 being Function of Omega1,REAL such that
A3: for x being set st x in Omega1 holds
F1 . x = H1(x) from FUNCT_2:sch_2(A2);
deffunc H2( set ) -> Element of REAL = P2 . {$1};
A4: for x being set st x in Omega2 holds
H2(x) in REAL ;
consider F2 being Function of Omega2,REAL such that
A5: for x being set st x in Omega2 holds
F2 . x = H2(x) from FUNCT_2:sch_2(A4);
A6: dom (Omega1 --> 1) = Omega1 by FUNCOP_1:13;
rng (Omega1 --> 1) c= REAL ;
then reconsider f1 = Omega1 --> 1 as Function of Omega1,REAL by A6, FUNCT_2:2;
for x being set st x in dom (Omega1 --> 1) holds
(Omega1 --> 1) . x = 1 by FUNCOP_1:7;
then A7: Integral ((P2M P1),f1) = (R_EAL 1) * ((P2M P1) . Omega1) by A6, MESFUNC6:97
.= 1 * (P1 . Omega1) by EXTREAL1:1
.= 1 by PROB_1:def_8 ;
consider G1 being FinSequence of REAL , s1 being FinSequence of Omega1 such that
A8: ( len G1 = card Omega1 & s1 is one-to-one & rng s1 = Omega1 & len s1 = card Omega1 & ( for n being Nat st n in dom G1 holds
G1 . n = (f1 . (s1 . n)) * (P1 . {(s1 . n)}) ) & Integral ((P2M P1),f1) = Sum G1 ) by RANDOM_1:13;
Omega1 c= Omega1 ;
then reconsider Y1 = Omega1 as finite Subset of Omega1 ;
dom F1 = Y1 by FUNCT_2:def_1;
then A9: dom (F1 * s1) = dom s1 by A8, RELAT_1:27;
A10: dom G1 = Seg (len s1) by A8, FINSEQ_1:def_3
.= dom s1 by FINSEQ_1:def_3 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_G1_holds_
G1_._x_=_(F1_*_s1)_._x
let x be set ; ::_thesis: ( x in dom G1 implies G1 . x = (F1 * s1) . x )
assume A11: x in dom G1 ; ::_thesis: G1 . x = (F1 * s1) . x
then reconsider nx = x as Element of NAT ;
thus G1 . x = (f1 . (s1 . nx)) * (P1 . {(s1 . nx)}) by A8, A11
.= 1 * (P1 . {(s1 . nx)}) by A8, A10, A11, FUNCOP_1:7, FUNCT_1:3
.= F1 . (s1 . nx) by A3, A8, A10, A11, FUNCT_1:3
.= (F1 * s1) . x by A10, A11, FUNCT_1:13 ; ::_thesis: verum
end;
then G1 = Func_Seq (F1,s1) by A9, A10, FUNCT_1:2;
then A12: setopfunc (Y1,Omega1,REAL,F1,addreal) = 1 by A7, A8, Th10;
A13: dom (Omega2 --> 1) = Omega2 by FUNCOP_1:13;
rng (Omega2 --> 1) c= REAL ;
then reconsider f2 = Omega2 --> 1 as Function of Omega2,REAL by A13, FUNCT_2:2;
for x being set st x in dom (Omega2 --> 1) holds
(Omega2 --> 1) . x = 1 by FUNCOP_1:7;
then A14: Integral ((P2M P2),f2) = (R_EAL 1) * ((P2M P2) . Omega2) by A13, MESFUNC6:97
.= 1 * (P2 . Omega2) by EXTREAL1:1
.= 1 by PROB_1:def_8 ;
consider G2 being FinSequence of REAL , s2 being FinSequence of Omega2 such that
A15: ( len G2 = card Omega2 & s2 is one-to-one & rng s2 = Omega2 & len s2 = card Omega2 & ( for n being Nat st n in dom G2 holds
G2 . n = (f2 . (s2 . n)) * (P2 . {(s2 . n)}) ) & Integral ((P2M P2),f2) = Sum G2 ) by RANDOM_1:13;
Omega2 c= Omega2 ;
then reconsider Y2 = Omega2 as finite Subset of Omega2 ;
dom F2 = Y2 by FUNCT_2:def_1;
then A16: dom (F2 * s2) = dom s2 by A15, RELAT_1:27;
A17: dom G2 = Seg (len s2) by A15, FINSEQ_1:def_3
.= dom s2 by FINSEQ_1:def_3 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_G2_holds_
G2_._x_=_(F2_*_s2)_._x
let x be set ; ::_thesis: ( x in dom G2 implies G2 . x = (F2 * s2) . x )
assume A18: x in dom G2 ; ::_thesis: G2 . x = (F2 * s2) . x
then reconsider nx = x as Element of NAT ;
thus G2 . x = (f2 . (s2 . nx)) * (P2 . {(s2 . nx)}) by A15, A18
.= 1 * (P2 . {(s2 . nx)}) by A15, A17, A18, FUNCOP_1:7, FUNCT_1:3
.= F2 . (s2 . nx) by A5, A15, A17, A18, FUNCT_1:3
.= (F2 * s2) . x by A17, A18, FUNCT_1:13 ; ::_thesis: verum
end;
then A19: G2 = Func_Seq (F2,s2) by A16, A17, FUNCT_1:2;
reconsider Y3 = [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:] by ZFMISC_1:96;
A20: now__::_thesis:_for_x,_y_being_set_st_x_in_Y1_&_y_in_Y2_holds_
Q_._(x,y)_=_(F1_._x)_*_(F2_._y)
let x, y be set ; ::_thesis: ( x in Y1 & y in Y2 implies Q . (x,y) = (F1 . x) * (F2 . y) )
assume A21: ( x in Y1 & y in Y2 ) ; ::_thesis: Q . (x,y) = (F1 . x) * (F2 . y)
hence Q . (x,y) = (P1 . {x}) * (P2 . {y}) by A1
.= (F1 . x) * (P2 . {y}) by A21, A3
.= (F1 . x) * (F2 . y) by A21, A5 ;
::_thesis: verum
end;
thus P . [:Omega1,Omega2:] = setopfunc (Y3,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= (setopfunc (Y1,Omega1,REAL,F1,addreal)) * (setopfunc (Y2,Omega2,REAL,F2,addreal)) by Th12, A20
.= 1 by A19, A14, A15, Th10, A12 ; ::_thesis: verum
end;
Lm9: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let Q be Function of [:Omega1,Omega2:],REAL; ::_thesis: for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let P be Function of (bool [:Omega1,Omega2:]),REAL; ::_thesis: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) implies for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 ) )
assume A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) ; ::_thesis: for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
reconsider Y12 = [:Omega1,Omega2:] as finite Subset of [:Omega1,Omega2:] by SUBSET:3;
A2: now__::_thesis:_for_z_being_set_st_z_in_[:Omega1,Omega2:]_holds_
0_<=_Q_._z
let z be set ; ::_thesis: ( z in [:Omega1,Omega2:] implies 0 <= Q . z )
assume z in [:Omega1,Omega2:] ; ::_thesis: 0 <= Q . z
then consider x, y being set such that
A3: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def_2;
for xx being set st xx in {x} holds
xx in Omega1 by A3, TARSKI:def_1;
then A4: ( {x} is Event of Trivial-SigmaField Omega1 & ( for xx being set st xx in {y} holds
xx in Omega2 ) ) by A3, TARSKI:def_1, TARSKI:def_3;
then A5: {y} is Event of Trivial-SigmaField Omega2 by TARSKI:def_3;
A6: Q . z = Q . (x,y) by A3
.= (P1 . {x}) * (P2 . {y}) by A3, A1 ;
( 0 <= P1 . {x} & 0 <= P2 . {y} ) by A4, A5, PROB_1:def_8;
hence 0 <= Q . z by A6; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x c= [:Omega1,Omega2:] implies ( 0 <= P . x & P . x <= 1 ) )
assume x c= [:Omega1,Omega2:] ; ::_thesis: ( 0 <= P . x & P . x <= 1 )
then reconsider Y = x as finite Subset of [:Omega1,Omega2:] ;
for z being set st z in Y holds
0 <= Q . z by A2;
then 0 <= setopfunc (Y,[:Omega1,Omega2:],REAL,Q,addreal) by Th13;
hence 0 <= P . x by A1; ::_thesis: P . x <= 1
A7: setopfunc (Y,[:Omega1,Omega2:],REAL,Q,addreal) <= setopfunc (Y12,[:Omega1,Omega2:],REAL,Q,addreal) by A2, Th14;
setopfunc (Y12,[:Omega1,Omega2:],REAL,Q,addreal) = P . [:Omega1,Omega2:] by A1;
then setopfunc (Y,[:Omega1,Omega2:],REAL,Q,addreal) <= 1 by A7, A1, Lm8;
hence P . x <= 1 by A1; ::_thesis: verum
end;
definition
let Omega1, Omega2 be non empty finite set ;
let P1 be Probability of Trivial-SigmaField Omega1;
let P2 be Probability of Trivial-SigmaField Omega2;
func Product-Probability (Omega1,Omega2,P1,P2) -> Probability of Trivial-SigmaField [:Omega1,Omega2:] means :Def2: :: RANDOM_2:def 2
ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds it . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) );
existence
ex b1 being Probability of Trivial-SigmaField [:Omega1,Omega2:] ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) )
proof
consider Q being Function of [:Omega1,Omega2:],REAL such that
A1: for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) by Lm1;
consider P being Function of (bool [:Omega1,Omega2:]),REAL such that
A2: for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) by Lm3;
A3: for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 ) by Lm9, A1, A2;
P . [:Omega1,Omega2:] = 1 by A1, A2, Lm8;
then P is Probability of Trivial-SigmaField [:Omega1,Omega2:] by A2, A3, Th8;
hence ex b1 being Probability of Trivial-SigmaField [:Omega1,Omega2:] ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Probability of Trivial-SigmaField [:Omega1,Omega2:] st ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) & ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) holds
b1 = b2
proof
let PP1, PP2 be Probability of Trivial-SigmaField [:Omega1,Omega2:]; ::_thesis: ( ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) & ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) implies PP1 = PP2 )
assume A4: ex Q1 being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q1,addreal) ) ) ; ::_thesis: ( for Q being Function of [:Omega1,Omega2:],REAL holds
( ex x, y being set st
( x in Omega1 & y in Omega2 & not Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) or ex z being finite Subset of [:Omega1,Omega2:] st not PP2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) or PP1 = PP2 )
assume A5: ex Q2 being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q2,addreal) ) ) ; ::_thesis: PP1 = PP2
consider Q1 being Function of [:Omega1,Omega2:],REAL such that
A6: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q1,addreal) ) ) by A4;
consider Q2 being Function of [:Omega1,Omega2:],REAL such that
A7: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q2,addreal) ) ) by A5;
Q1 = Q2 by A6, A7, Lm2;
hence PP1 = PP2 by Lm4, A6, A7; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Product-Probability RANDOM_2:def_2_:_
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for b5 being Probability of Trivial-SigmaField [:Omega1,Omega2:] holds
( b5 = Product-Probability (Omega1,Omega2,P1,P2) iff ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b5 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) );
theorem Th16: :: RANDOM_2:16
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y1 be non empty finite Subset of Omega1; ::_thesis: for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y2 be non empty finite Subset of Omega2; ::_thesis: (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
set P = Product-Probability (Omega1,Omega2,P1,P2);
consider Q being Function of [:Omega1,Omega2:],REAL such that
A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds (Product-Probability (Omega1,Omega2,P1,P2)) . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) by Def2;
thus (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2) by Lm7, A1; ::_thesis: verum
end;
theorem :: RANDOM_2:17
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
proof
let Omega1, Omega2 be non empty finite set ; ::_thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
let P1 be Probability of Trivial-SigmaField Omega1; ::_thesis: for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
let P2 be Probability of Trivial-SigmaField Omega2; ::_thesis: for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
let y1, y2 be set ; ::_thesis: ( y1 in Omega1 & y2 in Omega2 implies (Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2}) )
assume A1: ( y1 in Omega1 & y2 in Omega2 ) ; ::_thesis: (Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
then A2: {y1} is finite Subset of Omega1 by ZFMISC_1:31;
for yy being set st yy in {y2} holds
yy in Omega2 by A1, TARSKI:def_1;
then A3: {y2} is finite Subset of Omega2 by TARSKI:def_3;
[:{y1},{y2}:] = {[y1,y2]} by ZFMISC_1:29;
hence (Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2}) by Th16, A2, A3; ::_thesis: verum
end;
begin
definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
func Real-Valued-Random-Variables-Set Sigma -> non empty Subset of (RAlgebra Omega) equals :: RANDOM_2:def 3
{ f where f is Real-Valued-Random-Variable of Sigma : verum } ;
correctness
coherence
{ f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega);
proof
A1: not { f where f is Real-Valued-Random-Variable of Sigma : verum } is empty
proof
set g = the Real-Valued-Random-Variable of Sigma;
the Real-Valued-Random-Variable of Sigma in { f where f is Real-Valued-Random-Variable of Sigma : verum } ;
hence not { f where f is Real-Valued-Random-Variable of Sigma : verum } is empty ; ::_thesis: verum
end;
{ f where f is Real-Valued-Random-Variable of Sigma : verum } c= Funcs (Omega,REAL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Real-Valued-Random-Variable of Sigma : verum } or x in Funcs (Omega,REAL) )
assume x in { f where f is Real-Valued-Random-Variable of Sigma : verum } ; ::_thesis: x in Funcs (Omega,REAL)
then consider f being Real-Valued-Random-Variable of Sigma such that
A2: x = f ;
thus x in Funcs (Omega,REAL) by A2, FUNCT_2:8; ::_thesis: verum
end;
hence { f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega) by A1; ::_thesis: verum
end;
end;
:: deftheorem defines Real-Valued-Random-Variables-Set RANDOM_2:def_3_:_
for Omega being non empty set
for Sigma being SigmaField of Omega holds Real-Valued-Random-Variables-Set Sigma = { f where f is Real-Valued-Random-Variable of Sigma : verum } ;
Lm10: for Omega being non empty set
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 )
proof
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 set 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 set 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: - 1 is Real by XREAL_0:def_1;
then A16: - v1 is Real-Valued-Random-Variable of Sigma by RANDOM_1:20;
reconsider h = - v as Element of Funcs (Omega,REAL) ;
A17: h = (- 1) * v by A13, RLVECT_1:16;
A18: now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_-_(v1_._x)
let x be set ; ::_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 A17, A14, A15, 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 A18, VALUED_1:9;
hence - v in Real-Valued-Random-Variables-Set Sigma by A16; ::_thesis: verum
end;
then A19: 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
A20: u1 = u ;
reconsider h = a * u as Element of Funcs (Omega,REAL) ;
A21: ( 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 set st x in dom h holds
h . x = a * (u1 . x) by A20, FUNCSDOM:4;
then a * u = a (#) u1 by A21, 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, A19, 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
end;
registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster Real-Valued-Random-Variables-Set Sigma -> non empty multiplicatively-closed additively-linearly-closed ;
coherence
( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed ) by Lm10;
end;
definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
func R_Algebra_of_Real-Valued-Random-Variables Sigma -> Algebra equals :: RANDOM_2:def 4
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))) #);
coherence
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))) #) is Algebra by C0SP1:6;
end;
:: 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))) #);
registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster R_Algebra_of_Real-Valued-Random-Variables Sigma -> scalar-unital ;
coherence
R_Algebra_of_Real-Valued-Random-Variables Sigma is scalar-unital
proof
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
end;
end;