:: RANDOM_2 semantic presentation

REAL is non empty non trivial non finite V139() V140() V141() V145() set
NAT is non empty non trivial V17() V18() V19() non finite cardinal limit_cardinal V139() V140() V141() V142() V143() V144() V145() Element of bool REAL
bool REAL is non empty non trivial non finite set
ExtREAL is non empty V140() set
is Relation-like non empty non trivial non finite V147() set
bool is non empty non trivial non finite set
bool ExtREAL is non empty set
NAT is non empty non trivial V17() V18() V19() non finite cardinal limit_cardinal V139() V140() V141() V142() V143() V144() V145() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V139() V145() set
RAT is non empty non trivial non finite V139() V140() V141() V142() V145() set
INT is non empty non trivial non finite V139() V140() V141() V142() V143() V145() set

1 is non empty V17() V18() V19() V23() ext-real positive non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
{{},1} is non empty finite V31() V139() V140() V141() V142() V143() V144() set
is Relation-like non empty non trivial non finite V146() V147() V148() set
bool is non empty non trivial non finite set
bool () is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V146() V147() V148() set
bool is non empty non trivial non finite set
bool RAT is non empty non trivial non finite set
K435(NAT) is V187() set
is Relation-like non empty non trivial non finite V146() set
bool is non empty non trivial non finite set

bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V146() V147() V148() set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial non finite V146() V147() V148() set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial non finite V146() V147() V148() set
bool is non empty non trivial non finite set

bool is non empty non trivial non finite set

bool is non empty non trivial non finite set
is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set

bool is non empty non trivial non finite set
K721() is set
2 is non empty V17() V18() V19() V23() ext-real positive non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT

{ } is set
3 is non empty V17() V18() V19() V23() ext-real positive non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT

- 1 is non empty ext-real non positive negative V38() V39() Element of REAL
K473() is non empty ext-real non positive negative V39() Element of ExtREAL
K472() is non empty ext-real positive non negative V39() Element of ExtREAL
+infty is non empty ext-real positive non negative V39() set
-infty is non empty ext-real non positive negative V39() set

Seg 1 is non empty trivial finite 1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b1 where b1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V31() 1 -element V139() V140() V141() V142() V143() V144() set
Seg 2 is non empty finite 2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b1 where b1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V31() V139() V140() V141() V142() V143() V144() set

dom Omega is set
bool (dom Omega) is non empty set
Sigma is Element of bool (dom Omega)
v is Element of bool (dom Omega)
Omega | Sigma is Relation-like Function-like set
rng (Omega | Sigma) is set
Omega | v is Relation-like Function-like set
rng (Omega | v) is set
v1 is set
dom (Omega | Sigma) is set
g is set
(Omega | Sigma) . g is set
dom (Omega | v) is set
u is set
(Omega | v) . u is set
Omega . g is set
Omega . u is set
Sigma /\ v is Element of bool (dom Omega)

Sigma (#) Omega is Relation-like Function-like set
rng (Sigma (#) Omega) is set
rng Sigma is set
Omega | (rng Sigma) is Relation-like Function-like set
rng (Omega | (rng Sigma)) is set
v is set
dom (Sigma (#) Omega) is set
v1 is set
(Sigma (#) Omega) . v1 is set
dom Sigma is set
Sigma . v1 is set
dom Omega is set
g is set
Omega . g is set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)

v1 is set

dom () is non empty Element of bool Omega
() . v1 is ext-real V38() V39() Element of REAL
the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma . v1 is ext-real V38() V39() Element of REAL
abs () is ext-real V38() V39() Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)

v1 is set
dom (abs v) is non empty Element of bool Omega
(abs v) . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
abs (v . v1) is ext-real V38() V39() Element of REAL
Omega is non empty set
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty total quasi_total V146() V147() V148() V149() Element of bool [:Omega,NAT:]
[:Omega,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Omega,NAT:] is non empty non trivial non finite set
chi (Omega,Omega) is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is Relation-like non empty V147() set
bool [:Omega,ExtREAL:] is non empty set
dom (chi (Omega,Omega)) is Element of bool Omega
bool Omega is non empty set
dom (Omega --> 1) is non empty Element of bool Omega
v is set
(chi (Omega,Omega)) . v is ext-real Element of ExtREAL
(Omega --> 1) . v is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
(chi (Omega,Omega)) . v is ext-real Element of ExtREAL
(Omega --> 1) . v is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is ext-real V38() V39() Element of REAL
Omega --> Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
v is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty total quasi_total V146() V147() V148() V149() Element of bool [:Omega,NAT:]
[:Omega,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Omega,NAT:] is non empty non trivial non finite set
dom (Omega --> 1) is non empty Element of bool Omega
rng (Omega --> 1) is non empty V139() V140() V141() V142() V143() V144() Element of bool REAL
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]

[:Omega,ExtREAL:] is Relation-like non empty V147() set
bool [:Omega,ExtREAL:] is non empty set
u is Element of v
chi (u,Omega) is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
dom (Omega --> Sigma) is non empty Element of bool Omega
dom u1 is non empty Element of bool Omega
h is set
(Omega --> Sigma) . h is ext-real V38() V39() Element of REAL
Sigma * 1 is ext-real V38() V39() Element of REAL
u1 . h is ext-real V38() V39() Element of REAL
Sigma * (u1 . h) is ext-real V38() V39() Element of REAL
Sigma (#) u1 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Omega is non empty set
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) Sigma is Relation-like Function-like set
(- Sigma) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
abs Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(abs Sigma) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (- Sigma) is Element of bool Omega
bool Omega is non empty set
dom Sigma is Element of bool Omega
dom ((- Sigma) to_power 2) is Element of bool Omega
dom (Sigma to_power 2) is Element of bool Omega
dom (abs Sigma) is Element of bool Omega
dom ((abs Sigma) to_power 2) is Element of bool Omega
v is Element of Omega
(Sigma to_power 2) . v is ext-real V38() V39() Element of REAL
((- Sigma) to_power 2) . v is ext-real V38() V39() Element of REAL
((abs Sigma) to_power 2) . v is ext-real V38() V39() Element of REAL
(- Sigma) . v is ext-real V38() V39() Element of REAL
((- Sigma) . v) to_power 2 is ext-real V38() V39() Element of REAL
Sigma . v is ext-real V38() V39() Element of REAL
- (Sigma . v) is ext-real V38() V39() Element of REAL
(- (Sigma . v)) to_power 2 is ext-real V38() V39() Element of REAL
(Sigma . v) to_power 2 is ext-real V38() V39() Element of REAL
(abs Sigma) . v is ext-real V38() V39() Element of REAL
((abs Sigma) . v) to_power 2 is ext-real V38() V39() Element of REAL
abs (Sigma . v) is ext-real V38() V39() Element of REAL
(abs (Sigma . v)) to_power 2 is ext-real V38() V39() Element of REAL
v is Element of Omega
(Sigma to_power 2) . v is ext-real V38() V39() Element of REAL
((- Sigma) to_power 2) . v is ext-real V38() V39() Element of REAL
v1 is Element of Omega
(Sigma to_power 2) . v1 is ext-real V38() V39() Element of REAL
((abs Sigma) to_power 2) . v1 is ext-real V38() V39() Element of REAL
Omega is non empty set
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma + v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(Sigma + v) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma (#) v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
2 (#) (Sigma (#) v) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(Sigma to_power 2) + (2 (#) (Sigma (#) v)) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
v to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma - v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]

K105(1) is non empty ext-real non positive negative V38() V39() set

Sigma + (- v) is Relation-like Function-like set
(Sigma - v) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(Sigma to_power 2) - (2 (#) (Sigma (#) v)) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- (2 (#) (Sigma (#) v)) is Relation-like Function-like V146() set
K105(1) (#) (2 (#) (Sigma (#) v)) is Relation-like Function-like set
(Sigma to_power 2) + (- (2 (#) (Sigma (#) v))) is Relation-like Function-like set
((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (Sigma to_power 2) is Element of bool Omega
bool Omega is non empty set
dom Sigma is Element of bool Omega
v1 is Element of Omega
(Sigma to_power 2) . v1 is ext-real V38() V39() Element of REAL
Sigma . v1 is ext-real V38() V39() Element of REAL
(Sigma . v1) to_power 2 is ext-real V38() V39() Element of REAL
dom (v to_power 2) is Element of bool Omega
dom v is Element of bool Omega
v1 is Element of Omega
(v to_power 2) . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
(v . v1) to_power 2 is ext-real V38() V39() Element of REAL
dom (2 (#) (Sigma (#) v)) is Element of bool Omega
dom (Sigma (#) v) is Element of bool Omega
(dom Sigma) /\ (dom v) is Element of bool Omega
v1 is Element of Omega
(2 (#) (Sigma (#) v)) . v1 is ext-real V38() V39() Element of REAL
(Sigma (#) v) . v1 is ext-real V38() V39() Element of REAL
2 * ((Sigma (#) v) . v1) is ext-real V38() V39() Element of REAL
Sigma . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
(Sigma . v1) * (v . v1) is ext-real V38() V39() Element of REAL
2 * ((Sigma . v1) * (v . v1)) is ext-real V38() V39() Element of REAL
2 * (Sigma . v1) is ext-real V38() V39() Element of REAL
(2 * (Sigma . v1)) * (v . v1) is ext-real V38() V39() Element of REAL
dom ((Sigma + v) to_power 2) is Element of bool Omega
dom (Sigma + v) is Element of bool Omega
dom ((Sigma - v) to_power 2) is Element of bool Omega
dom (Sigma - v) is Element of bool Omega
dom ((Sigma to_power 2) + (2 (#) (Sigma (#) v))) is Element of bool Omega
(dom Sigma) /\ (dom (2 (#) (Sigma (#) v))) is Element of bool Omega
dom ((Sigma to_power 2) - (2 (#) (Sigma (#) v))) is Element of bool Omega
dom (((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2)) is Element of bool Omega
(dom ((Sigma to_power 2) + (2 (#) (Sigma (#) v)))) /\ (dom v) is Element of bool Omega
((dom Sigma) /\ (dom (2 (#) (Sigma (#) v)))) /\ (dom v) is Element of bool Omega
((dom Sigma) /\ (dom v)) /\ (dom v) is Element of bool Omega
dom (((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2)) is Element of bool Omega
(dom ((Sigma to_power 2) - (2 (#) (Sigma (#) v)))) /\ (dom v) is Element of bool Omega
v1 is Element of Omega
((Sigma + v) to_power 2) . v1 is ext-real V38() V39() Element of REAL
(Sigma + v) . v1 is ext-real V38() V39() Element of REAL
((Sigma + v) . v1) to_power 2 is ext-real V38() V39() Element of REAL
Sigma . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
(Sigma . v1) + (v . v1) is ext-real V38() V39() Element of REAL
((Sigma . v1) + (v . v1)) to_power 2 is ext-real V38() V39() Element of REAL
((Sigma . v1) + (v . v1)) ^2 is ext-real V38() V39() Element of REAL
K104(((Sigma . v1) + (v . v1)),((Sigma . v1) + (v . v1))) is ext-real V38() V39() set
(Sigma . v1) ^2 is ext-real V38() V39() Element of REAL
K104((Sigma . v1),(Sigma . v1)) is ext-real V38() V39() set
2 * (Sigma . v1) is ext-real V38() V39() Element of REAL
(2 * (Sigma . v1)) * (v . v1) is ext-real V38() V39() Element of REAL
((Sigma . v1) ^2) + ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(v . v1) ^2 is ext-real V38() V39() Element of REAL
K104((v . v1),(v . v1)) is ext-real V38() V39() set
(((Sigma . v1) ^2) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
(Sigma . v1) to_power 2 is ext-real V38() V39() Element of REAL
((Sigma . v1) to_power 2) + ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
(v . v1) to_power 2 is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
(Sigma to_power 2) . v1 is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) + ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
(v to_power 2) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) + ((2 * (Sigma . v1)) * (v . v1))) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
(2 (#) (Sigma (#) v)) . v1 is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) + ((2 (#) (Sigma (#) v)) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) + ((2 (#) (Sigma (#) v)) . v1)) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) + (2 (#) (Sigma (#) v))) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) + (2 (#) (Sigma (#) v))) . v1) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2)) . v1 is ext-real V38() V39() Element of REAL
((Sigma - v) to_power 2) . v1 is ext-real V38() V39() Element of REAL
(Sigma - v) . v1 is ext-real V38() V39() Element of REAL
((Sigma - v) . v1) to_power 2 is ext-real V38() V39() Element of REAL
(Sigma . v1) - (v . v1) is ext-real V38() V39() Element of REAL
((Sigma . v1) - (v . v1)) to_power 2 is ext-real V38() V39() Element of REAL
((Sigma . v1) - (v . v1)) ^2 is ext-real V38() V39() Element of REAL
K104(((Sigma . v1) - (v . v1)),((Sigma . v1) - (v . v1))) is ext-real V38() V39() set
((Sigma . v1) ^2) - ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma . v1) ^2) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
((Sigma . v1) to_power 2) - ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) - ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) - ((2 * (Sigma . v1)) * (v . v1))) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) - ((2 (#) (Sigma (#) v)) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) - ((2 (#) (Sigma (#) v)) . v1)) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) - (2 (#) (Sigma (#) v))) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) - (2 (#) (Sigma (#) v))) . v1) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2)) . v1 is ext-real V38() V39() Element of REAL
v1 is Element of Omega
((Sigma + v) to_power 2) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2)) . v1 is ext-real V38() V39() Element of REAL
g is Element of Omega
((Sigma - v) to_power 2) . g is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2)) . g is ext-real V38() V39() Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)

v is Relation-like Sigma -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Probability of Sigma
P2M v is Relation-like Sigma -defined ExtREAL -valued Function-like non empty total quasi_total V147() V155() nonnegative V204(Omega,Sigma) Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is Relation-like non empty V147() set
bool [:Sigma,ExtREAL:] is non empty set

(abs v1) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
expect (v1,v) is ext-real V38() V39() Element of REAL
Omega --> (expect (v1,v)) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
g is Element of Sigma
(P2M v) . g is ext-real Element of ExtREAL
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty total quasi_total V146() V147() V148() V149() Element of bool [:Omega,NAT:]
[:Omega,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Omega,NAT:] is non empty non trivial non finite set
dom (Omega --> 1) is non empty Element of bool Omega
rng (Omega --> 1) is non empty V139() V140() V141() V142() V143() V144() Element of bool REAL

[:Omega,ExtREAL:] is Relation-like non empty V147() set
bool [:Omega,ExtREAL:] is non empty set
chi (g,Omega) is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
dom (Omega --> (expect (v1,v))) is non empty Element of bool Omega
dom y is non empty Element of bool Omega
y is set
(Omega --> (expect (v1,v))) . y is ext-real V38() V39() Element of REAL
(expect (v1,v)) * 1 is ext-real V38() V39() Element of REAL
y . y is ext-real V38() V39() Element of REAL
(expect (v1,v)) * (y . y) is ext-real V38() V39() Element of REAL
(expect (v1,v)) (#) y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma

K105(1) is non empty ext-real non positive negative V38() V39() set

v1 + (- y) is Relation-like Function-like set
- 1 is non empty ext-real non positive negative V38() V39() V104() V161() Element of INT
(- 1) (#) ((expect (v1,v)) (#) y) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]

2 * (expect (v1,v)) is ext-real V38() V39() Element of REAL
(2 * (expect (v1,v))) (#) v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
(- 1) (#) ((2 * (expect (v1,v))) (#) v1) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((abs v1) to_power 2) - ((2 * (expect (v1,v))) (#) v1) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- ((2 * (expect (v1,v))) (#) v1) is Relation-like Function-like V146() set
K105(1) (#) ((2 * (expect (v1,v))) (#) v1) is Relation-like Function-like set
((abs v1) to_power 2) + (- ((2 * (expect (v1,v))) (#) v1)) is Relation-like Function-like set
v1 to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((expect (v1,v)) (#) y) (#) v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
2 (#) (((expect (v1,v)) (#) y) (#) v1) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
(v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is Relation-like Function-like V146() set
K105(1) (#) (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is Relation-like Function-like set
(v1 to_power 2) + (- (2 (#) (((expect (v1,v)) (#) y) (#) v1))) is Relation-like Function-like set
((expect (v1,v)) (#) y) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) + (((expect (v1,v)) (#) y) to_power 2) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(v1 to_power 2) + (- ((2 * (expect (v1,v))) (#) v1)) is Relation-like Function-like set
(expect (v1,v)) * (expect (v1,v)) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (expect (v1,v))) (#) y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (v1 to_power 2) is Element of bool Omega
dom v1 is non empty Element of bool Omega
dom (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is non empty Element of bool Omega
dom (((expect (v1,v)) (#) y) (#) v1) is non empty Element of bool Omega
dom ((expect (v1,v)) (#) y) is non empty Element of bool Omega
(dom ((expect (v1,v)) (#) y)) /\ (dom v1) is Element of bool Omega
Omega /\ (dom v1) is Element of bool Omega
dom (((expect (v1,v)) (#) y) to_power 2) is Element of bool Omega
dom (((expect (v1,v)) * (expect (v1,v))) (#) y) is non empty Element of bool Omega
dom ((2 * (expect (v1,v))) (#) v1) is non empty Element of bool Omega
dom ((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) is Element of bool Omega
(dom v1) /\ (Omega /\ (dom v1)) is Element of bool Omega
(dom v1) /\ (dom v1) is Element of bool Omega
((dom v1) /\ (dom v1)) /\ Omega is Element of bool Omega
(dom v1) /\ Omega is Element of bool Omega
dom ((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) is Element of bool Omega
(dom (v1 to_power 2)) /\ (dom ((2 * (expect (v1,v))) (#) v1)) is Element of bool Omega
dom (((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) + (((expect (v1,v)) (#) y) to_power 2)) is Element of bool Omega
(dom ((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1)))) /\ (dom (((expect (v1,v)) (#) y) to_power 2)) is Element of bool Omega
Omega /\ Omega is set
(dom v1) /\ (Omega /\ Omega) is Element of bool Omega
dom (((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y)) is Element of bool Omega
f2 is Element of Omega
(((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) + (((expect (v1,v)) (#) y) to_power 2)) . f2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y)) . f2 is ext-real V38() V39() Element of REAL
((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) . f2 is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) to_power 2) . f2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) . f2) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
(v1 to_power 2) . f2 is ext-real V38() V39() Element of REAL
(2 (#) (((expect (v1,v)) (#) y) (#) v1)) . f2 is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - ((2 (#) (((expect (v1,v)) (#) y) (#) v1)) . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 (#) (((expect (v1,v)) (#) y) (#) v1)) . f2)) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) (#) v1) . f2 is ext-real V38() V39() Element of REAL
2 * ((((expect (v1,v)) (#) y) (#) v1) . f2) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) (#) v1) . f2)) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) (#) v1) . f2))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) (#) y) . f2 is ext-real V38() V39() Element of REAL
v1 . f2 is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) . f2) * (v1 . f2) is ext-real V38() V39() Element of REAL
2 * ((((expect (v1,v)) (#) y) . f2) * (v1 . f2)) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) . f2) * (v1 . f2))) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) . f2) * (v1 . f2)))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
y . f2 is ext-real V38() V39() Element of REAL
(expect (v1,v)) * (y . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (y . f2)) * (v1 . f2) is ext-real V38() V39() Element of REAL
2 * (((expect (v1,v)) * (y . f2)) * (v1 . f2)) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * (y . f2)) * (v1 . f2))) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * (y . f2)) * (v1 . f2)))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * 1) * (v1 . f2) is ext-real V38() V39() Element of REAL
2 * (((expect (v1,v)) * 1) * (v1 . f2)) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * 1) * (v1 . f2))) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * 1) * (v1 . f2)))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
(2 * (expect (v1,v))) * (v1 . f2) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2)) is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) . f2) to_power 2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((((expect (v1,v)) (#) y) . f2) to_power 2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (y . f2)) to_power 2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * (y . f2)) to_power 2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * 1) to_power 2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * 1) to_power 2) is ext-real V38() V39() Element of REAL
(expect (v1,v)) ^2 is ext-real V38() V39() Element of REAL
K104((expect (v1,v)),(expect (v1,v))) is ext-real V38() V39() set
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((expect (v1,v)) ^2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((expect (v1,v)) * (expect (v1,v))) is ext-real V38() V39() Element of REAL
((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) . f2 is ext-real V38() V39() Element of REAL
(((expect (v1,v)) * (expect (v1,v))) (#) y) . f2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) . f2) + ((((expect (v1,v)) * (expect (v1,v))) (#) y) . f2) is ext-real V38() V39() Element of REAL
((2 * (expect (v1,v))) (#) v1) . f2 is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (((2 * (expect (v1,v))) (#) v1) . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (((2 * (expect (v1,v))) (#) v1) . f2)) + ((((expect (v1,v)) * (expect (v1,v))) (#) y) . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((((expect (v1,v)) * (expect (v1,v))) (#) y) . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (expect (v1,v))) * (y . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * (expect (v1,v))) * (y . f2)) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (expect (v1,v))) * 1 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * (expect (v1,v))) * 1) is ext-real V38() V39() Element of REAL

(abs Y1) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
v1 - ((expect (v1,v)) (#) y) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- ((expect (v1,v)) (#) y) is Relation-like Function-like V146() set
K105(1) (#) ((expect (v1,v)) (#) y) is Relation-like Function-like set
v1 + (- ((expect (v1,v)) (#) y)) is Relation-like Function-like set
(v1 - ((expect (v1,v)) (#) y)) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(((abs v1) to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M v),((abs Y1) to_power 2)) is ext-real Element of ExtREAL

v1 - Y2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma

v1 + (- Y2) is Relation-like Function-like set

(abs s2) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
f2 is ext-real V38() V39() Element of REAL
Integral ((P2M v),((abs s2) to_power 2)) is ext-real Element of ExtREAL

v1 + (- x) is Relation-like Function-like set

(abs Y3) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
G2 is ext-real V38() V39() Element of REAL
Integral ((P2M v),((abs Y3) to_power 2)) is ext-real Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
v is Relation-like Sigma -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Probability of Sigma
P2M v is Relation-like Sigma -defined ExtREAL -valued Function-like non empty total quasi_total V147() V155() nonnegative V204(Omega,Sigma) Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is Relation-like non empty V147() set
bool [:Sigma,ExtREAL:] is non empty set
v1 is ext-real V38() V39() Element of REAL
v1 to_power 2 is ext-real V38() V39() Element of REAL

(abs g) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
expect (g,v) is ext-real V38() V39() Element of REAL
{ b1 where b1 is Element of Omega : v1 <= |.((g . b1) - (expect (g,v))).| } is set
v . { b1 where b1 is Element of Omega : v1 <= |.((g . b1) - (expect (g,v))).| } is ext-real V38() V39() Element of REAL
(Omega,Sigma,v,g) is ext-real V38() V39() Element of REAL
(Omega,Sigma,v,g) / (v1 to_power 2) is ext-real V38() V39() Element of REAL
{ b1 where b1 is Element of Omega : v1 to_power 2 <= (abs ((g . b1) - (expect (g,v)))) to_power 2 } is set
u is set
v1 ^2 is ext-real V38() V39() Element of REAL
K104(v1,v1) is ext-real V38() V39() set
g . u is ext-real V38() V39() Element of REAL
(g . u) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . u) - (expect (g,v)))) ^2 is ext-real V38() V39() Element of REAL
K104((abs ((g . u) - (expect (g,v)))),(abs ((g . u) - (expect (g,v))))) is ext-real V38() V39() set
(abs ((g . u) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
|.((g . u1) - (expect (g,v))).| is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
|.((g . u1) - (expect (g,v))).| is ext-real V38() V39() Element of REAL
u is set
g . u is ext-real V38() V39() Element of REAL
(g . u) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u) - (expect (g,v))) is ext-real V38() V39() Element of REAL
v1 ^2 is ext-real V38() V39() Element of REAL
K104(v1,v1) is ext-real V38() V39() set
(abs ((g . u) - (expect (g,v)))) ^2 is ext-real V38() V39() Element of REAL
K104((abs ((g . u) - (expect (g,v)))),(abs ((g . u) - (expect (g,v))))) is ext-real V38() V39() set
(abs ((g . u) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u1) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . u1) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u1) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . u1) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
Omega --> (expect (g,v)) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]

K105(1) is non empty ext-real non positive negative V38() V39() set

g + (- u1) is Relation-like Function-like set

(abs u) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
Integral ((P2M v),((abs u) to_power 2)) is ext-real Element of ExtREAL

{ b1 where b1 is Element of Omega : v1 to_power 2 <= h . b1 } is set
v . { b1 where b1 is Element of Omega : v1 to_power 2 <= h . b1 } is ext-real V38() V39() Element of REAL
expect (h,v) is ext-real V38() V39() Element of REAL
(expect (h,v)) / (v1 to_power 2) is ext-real V38() V39() Element of REAL
dom g is non empty Element of bool Omega
dom (Omega --> (expect (g,v))) is non empty Element of bool Omega
g - (Omega --> (expect (g,v))) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- (Omega --> (expect (g,v))) is Relation-like Function-like V146() set
K105(1) (#) (Omega --> (expect (g,v))) is Relation-like Function-like set
g + (- (Omega --> (expect (g,v)))) is Relation-like Function-like set
dom (g - (Omega --> (expect (g,v)))) is Element of bool Omega
(dom g) /\ (dom (Omega --> (expect (g,v)))) is Element of bool Omega
abs (g - (Omega --> (expect (g,v)))) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (abs (g - (Omega --> (expect (g,v))))) is Element of bool Omega
(abs (g - (Omega --> (expect (g,v))))) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom ((abs (g - (Omega --> (expect (g,v))))) to_power 2) is Element of bool Omega
y is set
h . y is ext-real V38() V39() Element of REAL
(abs (g - (Omega --> (expect (g,v))))) . y is ext-real V38() V39() Element of REAL
((abs (g - (Omega --> (expect (g,v))))) . y) to_power 2 is ext-real V38() V39() Element of REAL
(g - (Omega --> (expect (g,v)))) . y is ext-real V38() V39() Element of REAL
abs ((g - (Omega --> (expect (g,v)))) . y) is ext-real V38() V39() Element of REAL
(abs ((g - (Omega --> (expect (g,v)))) . y)) to_power 2 is ext-real V38() V39() Element of REAL
g . y is ext-real V38() V39() Element of REAL
(Omega --> (expect (g,v))) . y is ext-real V38() V39() Element of REAL
(g . y) - ((Omega --> (expect (g,v))) . y) is ext-real V38() V39() Element of REAL
abs ((g . y) - ((Omega --> (expect (g,v))) . y)) is ext-real V38() V39() Element of REAL
(abs ((g . y) - ((Omega --> (expect (g,v))) . y))) to_power 2 is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is set
h . y is ext-real V38() V39() Element of REAL
(abs (g - (Omega --> (expect (g,v))))) . y is ext-real V38() V39() Element of REAL
((abs (g - (Omega --> (expect (g,v))))) . y) to_power 2 is ext-real V38() V39() Element of REAL
(g - (Omega --> (expect (g,v)))) . y is ext-real V38() V39() Element of REAL
abs ((g - (Omega --> (expect (g,v)))) . y) is ext-real V38() V39() Element of REAL
(abs ((g - (Omega --> (expect (g,v)))) . y)) to_power 2 is ext-real V38() V39() Element of REAL
g . y is ext-real V38() V39() Element of REAL
(Omega --> (expect (g,v))) . y is ext-real V38() V39() Element of REAL
(g . y) - ((Omega --> (expect (g,v))) . y) is ext-real V38() V39() Element of REAL
abs ((g . y) - ((Omega --> (expect (g,v))) . y)) is ext-real V38() V39() Element of REAL
(abs ((g . y) - ((Omega --> (expect (g,v))) . y))) to_power 2 is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
Omega is non empty finite set
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
bool Omega is non empty finite V31() set
[:(bool Omega),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(bool Omega),REAL:] is non empty non trivial non finite set
Trivial-SigmaField Omega is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
bool (bool Omega) is non empty finite V31() set
Sigma is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v is Relation-like bool Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool Omega),REAL:]
v . Omega is ext-real V38() V39() Element of REAL
v1 is finite Event of Trivial-SigmaField Omega
g is finite Event of Trivial-SigmaField Omega
v1 \/ g is finite Event of Trivial-SigmaField Omega
v . (v1 \/ g) is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
v . g is ext-real V38() V39() Element of REAL
(v . v1) + (v . g) is ext-real V38() V39() Element of REAL
dom Sigma is non empty finite Element of bool Omega
u is finite Element of bool Omega
u1 is finite Element of bool Omega
u \/ u1 is finite Element of bool Omega
setopfunc ((u \/ u1),Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
setopfunc (u,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
setopfunc (u1,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
addreal . ((setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))) is ext-real V38() V39() Element of REAL
{(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))} is non empty finite V139() V140() V141() set
{(setopfunc (u,Omega,REAL,Sigma,addreal))} is non empty trivial finite 1 -element V139() V140() V141() set
{{(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))},{(setopfunc (u,Omega,REAL,Sigma,addreal))}} is non empty finite V31() set
addreal . [(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))] is ext-real V38() V39() set
addreal . ((setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)) is ext-real V38() V39() Element of REAL
[(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)] is set
{(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)} is non empty finite V139() V140() V141() set
{{(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)},{(setopfunc (u,Omega,REAL,Sigma,addreal))}} is non empty finite V31() set
addreal . [(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)] is ext-real V38() V39() set
addreal . ((v . v1),(v . g)) is ext-real V38() V39() Element of REAL
[(v . v1),(v . g)] is set
{(v . v1),(v . g)} is non empty finite V139() V140() V141() set
{(v . v1)} is non empty trivial finite 1 -element V139() V140() V141() set
{{(v . v1),(v . g)},{(v . v1)}} is non empty finite V31() set
addreal . [(v . v1),(v . g)] is ext-real V38() V39() set
v1 is finite Event of Trivial-SigmaField Omega
v . v1 is ext-real V38() V39() Element of REAL
K264(Omega) is non empty finite V31() Element of bool (bool Omega)
[:NAT,K264(Omega):] is Relation-like non empty non trivial non finite set
bool [:NAT,K264(Omega):] is non empty non trivial non finite set
v1 is Relation-like NAT -defined Trivial-SigmaField Omega -valued K264(Omega) -valued Function-like non empty total quasi_total Element of bool [:NAT,K264(Omega):]

lim (v * v1) is ext-real V38() V39() Element of REAL
Intersection v1 is finite Element of bool Omega
v . () is ext-real V38() V39() Element of REAL
g is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
dom v1 is non empty V139() V140() V141() V142() V143() V144() Element of bool NAT
(v * v1) . u is ext-real V38() V39() Element of REAL
v1 . u is finite Element of Trivial-SigmaField Omega
v . (v1 . u) is ext-real V38() V39() Element of REAL
Omega is non empty finite set
Trivial-SigmaField Omega is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
bool Omega is non empty finite V31() set
bool (bool Omega) is non empty finite V31() set
Sigma is non empty finite set
Trivial-SigmaField Sigma is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Sigma) Element of bool (bool Sigma)
bool Sigma is non empty finite V31() set
bool (bool Sigma) is non empty finite V31() set
[:Omega,Sigma:] is Relation-like non empty finite set
[:[:Omega,Sigma:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:Omega,Sigma:],REAL:] is non empty non trivial non finite set

dom g is set
u is set
g . u is set
u1 is set
h is set
[u1,h] is set
{u1,h} is non empty finite set
{u1} is non empty trivial finite 1 -element set
{{u1,h},{u1}} is non empty finite V31() set
g . (u1,h) is set
g . [u1,h] is set
v . {u1} is ext-real V38() V39() Element of REAL
{h} is non empty trivial finite 1 -element set
v1 . {h} is ext-real V38() V39() Element of REAL
(v . {u1}) * (v1 . {h}) is ext-real V38() V39() Element of REAL
u is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
u1 is set
h is set
u . (u1,h) is set
[u1,h] is set
{u1,h} is non empty finite set
{u1} is non empty trivial finite 1 -element set
{{u1,h},{u1}} is non empty finite V31() set
u . [u1,h] is ext-real V38() V39() set
v . {u1} is ext-real V38() V39() Element of REAL
{h} is non empty trivial finite 1 -element set
v1 . {h} is ext-real V38() V39() Element of REAL
(v . {u1}) * (v1 . {h}) is ext-real V38() V39() Element of REAL
Omega is non empty finite set
Trivial-SigmaField Omega is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
bool Omega is non empty finite V31() set
bool (bool Omega) is non empty finite V31() set
Sigma is non empty finite set
Trivial-SigmaField Sigma is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Sigma) Element of bool (bool Sigma)
bool Sigma is non empty finite V31() set
bool (bool Sigma) is non empty finite V31() set
[:Omega,Sigma:] is Relation-like non empty finite set
[:[:Omega,Sigma:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:Omega,Sigma:],REAL:] is non empty non trivial non finite set

g is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
u is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
dom g is Relation-like Omega -defined Sigma -valued non empty finite Element of bool [:Omega,Sigma:]
bool [:Omega,Sigma:] is non empty finite V31() set
dom u is Relation-like Omega -defined Sigma -valued non empty finite Element of bool [:Omega,Sigma:]
u1 is set
h is set
y is set
[h,y] is set
{h,y} is non empty finite set
{h} is non empty trivial finite 1 -element set
{{h,y},{h}} is non empty finite V31()