:: 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;