:: 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
[:NAT,ExtREAL:] is Relation-like non empty non trivial non finite V147() set
bool [:NAT,ExtREAL:] 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
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V18() V19() V21() V22() V23() ext-real non positive non negative finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V38() V39() V139() V140() V141() V142() V143() V144() V145() V146() V147() V148() V149() 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
[:NAT,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:REAL,REAL:] is non empty non trivial non finite set
bool RAT is non empty non trivial non finite set
K435(NAT) is V187() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V146() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V146() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V146() V147() V148() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V146() V147() V148() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:[:NAT,NAT:],NAT:] 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
1 -tuples_on NAT is FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = 1 } 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
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V18() V19() V21() V22() V23() ext-real non positive non negative finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V38() V39() V104() V139() V140() V141() V142() V143() V144() V145() V146() V147() V148() V149() 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
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() V222( REAL ) V223( REAL ) V247( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
Seg 1 is non empty trivial finite 1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty finite V31() V139() V140() V141() V142() V143() V144() set
Omega is Relation-like Function-like one-to-one 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 is Relation-like Function-like set
Omega is Relation-like Function-like set
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)
the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 is set
abs the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
dom (abs the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma) is non empty Element of bool Omega
(abs 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
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 ( 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
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 Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
abs v is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
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:]
R_EAL u1 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
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:]
- v is Relation-like Function-like V146() set
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) v is Relation-like Function-like 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)
v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
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 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(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
y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
R_EAL y 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
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
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 - y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- y is Relation-like Function-like V146() set
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) y is Relation-like Function-like 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:]
Y1 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)) 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 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(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
Y2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
s2 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 Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- Y2 is Relation-like Function-like V146() set
K105(1) (#) Y2 is Relation-like Function-like set
v1 + (- Y2) is Relation-like Function-like set
abs s2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(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
x is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
Y3 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 - x is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- x is Relation-like Function-like V146() set
K105(1) (#) x is Relation-like Function-like set
v1 + (- x) is Relation-like Function-like set
abs Y3 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(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
g is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
abs g is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(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
{ b₁ where b₁ is Element of Omega : v1 <= |.((g . b₁) - (expect (g,v))).| } is set
v . { b₁ where b₁ is Element of Omega : v1 <= |.((g . b₁) - (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
{ b₁ where b₁ is Element of Omega : v1 to_power 2 <= (abs ((g . b₁) - (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:]
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
u is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
g - u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- u1 is Relation-like Function-like V146() set
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) u1 is Relation-like Function-like set
g + (- u1) is Relation-like Function-like set
abs u is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(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
h is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
{ b₁ where b₁ is Element of Omega : v1 to_power 2 <= h . b₁ } is set
v . { b₁ where b₁ is Element of Omega : v1 to_power 2 <= h . b₁ } 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 set
{(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):]
v * v1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:NAT,REAL:]
lim (v * v1) is ext-real V38() V39() Element of REAL
Intersection v1 is finite Element of bool Omega
v . (Intersection v1) 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
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
g is Relation-like Function-like 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
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
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() set
g . u1 is ext-real V38() V39() Element of REAL
g . (h,y) is set
g . [h,y] is ext-real V38() V39() set
v . {h} is ext-real V38() V39() Element of REAL
{y} is non empty trivial finite 1 -element set
v1 . {y} is ext-real V38() V39() Element of REAL
(v . {h}) * (v1 . {y}) is ext-real V38() V39() Element of REAL
u . (h,y) is set
u . [h,y] is ext-real V38() V39() set
u . u1 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
bool [:Omega,Sigma:] is non empty finite V31() set
[:(bool [:Omega,Sigma:]),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(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 set
u1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (u1,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
u is Relation-like bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
u1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
u . u1 is ext-real V38() V39() Element of REAL
setopfunc (u1,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
h is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (h,[:Omega,Sigma:],REAL,g,addreal) 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
bool [:Omega,Sigma:] is non empty finite V31() set
[:(bool [:Omega,Sigma:]),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(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 bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
u1 is Relation-like bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
h is set
u . h is ext-real V38() V39() Element of REAL
y is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (y,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
u1 . h is ext-real V38() V39() Element of REAL
Sigma is non empty set
Omega is non empty set
[:Sigma,Omega:] is Relation-like non empty set
bool [:Sigma,Omega:] is non empty set
v is Relation-like Sigma -defined Omega -valued Function-like non empty total quasi_total Element of bool [:Sigma,Omega:]
v1 is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
v * v1 is Relation-like NAT -defined Omega -valued Function-like finite Element of bool [:NAT,Omega:]
[:NAT,Omega:] is Relation-like non empty non trivial non finite set
bool [:NAT,Omega:] is non empty non trivial non finite set
g is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
v * g is Relation-like NAT -defined Omega -valued Function-like finite Element of bool [:NAT,Omega:]
v1 ^ g is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
v * (v1 ^ g) is Relation-like NAT -defined Omega -valued Function-like finite Element of bool [:NAT,Omega:]
u is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
u1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
u ^ u1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
dom u is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom v1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom u1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom g is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
len 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
len v1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
len u1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
len 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
dom (u ^ u1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
(len v1) + (len 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
Seg ((len v1) + (len g)) is finite (len v1) + (len g) -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= (len v1) + (len g) ) } is set
dom (v * (v1 ^ g)) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom (v1 ^ g) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
h is set
(u ^ u1) . h is set
(v * (v1 ^ g)) . h is set
y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(v * (v1 ^ g)) . y is set
(v1 ^ g) . y is set
v . ((v1 ^ g) . y) is set
Seg (len v1) is finite len v1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len v1 ) } is set
v1 . y is set
v . (v1 . y) is set
u . y is set
len (v1 ^ 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
y - (len v1) is ext-real V38() V39() V104() V161() Element of INT
g . (y - (len v1)) is set
((len v1) + (len g)) - (len v1) is ext-real V38() V39() V104() V161() Element of INT
(len v1) - (len v1) is ext-real V38() V39() V104() V161() Element of INT
Seg (len g) is finite len g -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len g ) } is set
len (u ^ u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u1 . (y - (len v1)) is set
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
bool Omega is non empty set
Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v is finite Element of bool Omega
setopfunc (v,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
dom Sigma is non empty Element of bool Omega
v1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng v1 is finite Element of bool Omega
Func_Seq (Sigma,v1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
v1 (#) Sigma is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
addreal "**" (Func_Seq (Sigma,v1)) is ext-real V38() V39() Element of REAL
Sum (Func_Seq (Sigma,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
bool Omega is non empty set
Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v is finite Element of bool Omega
setopfunc (v,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
v1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng v1 is finite Element of bool Omega
Func_Seq (Sigma,v1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
v1 (#) Sigma is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (Sigma,v1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (Sigma,v1)) is ext-real V38() V39() Element of REAL
dom Sigma is non empty Element of bool Omega
Omega is Relation-like Function-like set
dom Omega is set
Omega . 1 is set
<*(Omega . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,(Omega . 1)] is set
{1,(Omega . 1)} is non empty finite set
{{1,(Omega . 1)},{1}} is non empty finite V31() set
{[1,(Omega . 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
Sigma is set
rng Omega is set
{Sigma} is non empty trivial finite 1 -element set
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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 non empty set
[:Sigma,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Sigma,REAL:] is non empty non trivial non finite set
[:Omega,Sigma:] is Relation-like non empty 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
bool Omega is non empty set
bool Sigma is non empty set
bool [:Omega,Sigma:] is non empty set
v is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v1 is Relation-like Sigma -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Sigma,REAL:]
g is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
u is non empty finite Element of bool Omega
u1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng u1 is finite Element of bool Omega
Func_Seq (v,u1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
u1 (#) v is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v,u1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v,u1)) is ext-real V38() V39() Element of REAL
h is set
dom u1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng y is finite Element of bool Sigma
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng y is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
Func_Seq (g,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
s1 is non empty finite Element of bool Sigma
[:u,s1:] is Relation-like non empty finite set
Y1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng y is finite Element of bool Sigma
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng y is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
Func_Seq (g,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
s1 is non empty finite Element of bool Sigma
[:u,s1:] is Relation-like non empty finite set
Y1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
y . 1 is set
<*(y . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,(y . 1)] is set
{1,(y . 1)} is non empty finite set
{{1,(y . 1)},{1}} is non empty finite V31() set
{[1,(y . 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{(y . 1)} is non empty trivial finite 1 -element set
v1 * y is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
(v1 * y) . 1 is ext-real V38() V39() Element of REAL
dom v1 is non empty Element of bool Sigma
dom (v1 * y) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom y is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
<*((v1 * y) . 1)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V146() V147() V148() V150() V151() V152() V153() FinSequence of REAL
[1,((v1 * y) . 1)] is set
{1,((v1 * y) . 1)} is non empty finite V139() V140() V141() set
{{1,((v1 * y) . 1)},{1}} is non empty finite V31() set
{[1,((v1 * y) . 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
[:u,{(y . 1)}:] is Relation-like non empty finite set
len u1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
card u 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
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
card (rng y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (card u) is non empty finite card u -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= card u ) } is set
dom y is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s2 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 s2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len y) is finite len y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len y ) } is set
Y2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
u1 . Y2 is set
[(u1 . Y2),(y . 1)] is set
{(u1 . Y2),(y . 1)} is non empty finite set
{(u1 . Y2)} is non empty trivial finite 1 -element set
{{(u1 . Y2),(y . 1)},{(u1 . Y2)}} is non empty finite V31() set
s2 . Y2 is set
rng s2 is finite set
Y3 is set
Y2 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
dom Y2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
x is set
Y2 . Y3 is set
Y2 . x is set
y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u1 . y is set
[(u1 . y),(y . 1)] is set
{(u1 . y),(y . 1)} is non empty finite set
{(u1 . y)} is non empty trivial finite 1 -element set
{{(u1 . y),(y . 1)},{(u1 . y)}} is non empty finite V31() set
Y2 . y is set
Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u1 . Y33 is set
[(u1 . Y33),(y . 1)] is set
{(u1 . Y33),(y . 1)} is non empty finite set
{(u1 . Y33)} is non empty trivial finite 1 -element set
{{(u1 . Y33),(y . 1)},{(u1 . Y33)}} is non empty finite V31() set
rng Y2 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
Y3 is set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V31() set
Y33 is set
u1 . Y33 is set
Q0 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y2 . Q0 is set
[:(dom y),(dom y):] is Relation-like RAT -valued INT -valued finite V146() V147() V148() V149() set
bool [:(dom y),(dom y):] is non empty finite V31() set
Y3 is Relation-like dom y -defined dom y -valued Function-like one-to-one finite total quasi_total onto bijective V146() V147() V148() V149() Element of bool [:(dom y),(dom y):]
y * Y3 is Relation-like dom y -defined [:Omega,Sigma:] -valued Function-like finite Element of bool [:(dom y),[:Omega,Sigma:]:]
[:(dom y),[:Omega,Sigma:]:] is Relation-like set
bool [:(dom y),[:Omega,Sigma:]:] is non empty set
dom Y3 is finite V139() V140() V141() V142() V143() V144() Element of bool (dom y)
bool (dom y) is non empty finite V31() set
rng Y3 is finite V139() V140() V141() V142() V143() V144() Element of bool REAL
Func_Seq (g,Y2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Y2 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
(Func_Seq (g,y)) * Y3 is Relation-like dom y -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:(dom y),REAL:]
[:(dom y),REAL:] is Relation-like V146() V147() V148() set
bool [:(dom y),REAL:] is non empty set
dom g is Relation-like Omega -defined Sigma -valued non empty Element of bool [:Omega,Sigma:]
dom (Func_Seq (g,y)) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum (Func_Seq (g,Y2)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,Y2)) is ext-real V38() V39() Element of REAL
dom v is non empty Element of bool Omega
v * u1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (v * u1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len u1) is finite len u1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len u1 ) } is set
g * Y2 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (g * Y2) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
((v1 * y) . 1) (#) (v * u1) is Relation-like NAT -defined REAL -valued Function-like V146() V147() V148() Element of bool [:NAT,REAL:]
dom (((v1 * y) . 1) (#) (v * u1)) is V139() V140() V141() V142() V143() V144() Element of bool NAT
x is set
len Y2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (len Y2) is finite len Y2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Y2 ) } is set
y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u1 /. y is Element of Omega
u1 . y is set
Y2 . y is set
[(u1 . y),(y . 1)] is set
{(u1 . y),(y . 1)} is non empty finite set
{(u1 . y)} is non empty trivial finite 1 -element set
{{(u1 . y),(y . 1)},{(u1 . y)}} is non empty finite V31() set
[(u1 /. y),(y . 1)] is set
{(u1 /. y),(y . 1)} is non empty finite set
{(u1 /. y)} is non empty trivial finite 1 -element set
{{(u1 /. y),(y . 1)},{(u1 /. y)}} is non empty finite V31() set
v1 . (y . 1) is ext-real V38() V39() Element of REAL
(g * Y2) . x is ext-real V38() V39() Element of REAL
g . ((u1 /. y),(y . 1)) is set
g . [(u1 /. y),(y . 1)] is ext-real V38() V39() set
v . (u1 /. y) is ext-real V38() V39() Element of REAL
(v . (u1 /. y)) * ((v1 * y) . 1) is ext-real V38() V39() Element of REAL
(v * u1) . y is ext-real V38() V39() Element of REAL
((v * u1) . y) * ((v1 * y) . 1) is ext-real V38() V39() Element of REAL
(((v1 * y) . 1) (#) (v * u1)) . x is ext-real V38() V39() Element of REAL
((v1 * y) . 1) * (Func_Seq (v,u1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
((v1 * y) . 1) multreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:REAL,REAL:]
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() V222( REAL ) V223( REAL ) V247( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total V146() V147() V148() V150() V152() Element of bool [:REAL,REAL:]
multreal [;] (((v1 * y) . 1),(id REAL)) is set
(Func_Seq (v,u1)) (#) (((v1 * y) . 1) multreal) is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
y + 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
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng y is finite Element of bool Sigma
Y1 is non empty finite Element of bool Sigma
s1 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng s1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
f2 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
[:u,Y1:] is Relation-like non empty finite set
Func_Seq (g,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s1 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng y is finite Element of bool Sigma
Y1 is non empty finite Element of bool Sigma
s1 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng s1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
f2 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
[:u,Y1:] is Relation-like non empty finite set
len u1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len y) * (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Y2 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 Y2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg ((len y) * (len u1)) is finite (len y) * (len u1) -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= (len y) * (len u1) ) } is set
Seg (len u1) is finite len u1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len u1 ) } is set
y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
y -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(y -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((y -' 1) div (len u1)) + 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
(y -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((y -' 1) mod (len u1)) + 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
((len y) * (len u1)) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((len y) * (len u1)) -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
Y3 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
Y3 * x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
0 + 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
(Y3 * x) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y3 * x) -' 1) div x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Y3 * x) div x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y3 * x) div x) - 1 is ext-real V38() V39() V104() V161() Element of INT
((len y) * (len u1)) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
pp1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
Seg pp1 is finite pp1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= pp1 ) } is set
dom y is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
pp2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
(y -' 1) mod pp2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg pp2 is finite pp2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= pp2 ) } is set
Y3 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
Y3 -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Y3 -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y3 -' 1) div (len u1)) + 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
(Y3 -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y3 -' 1) mod (len u1)) + 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
y . (((Y3 -' 1) div (len u1)) + 1) is set
u1 . (((Y3 -' 1) mod (len u1)) + 1) is set
[(u1 . (((Y3 -' 1) mod (len u1)) + 1)),(y . (((Y3 -' 1) div (len u1)) + 1))] is set
{(u1 . (((Y3 -' 1) mod (len u1)) + 1)),(y . (((Y3 -' 1) div (len u1)) + 1))} is non empty finite set
{(u1 . (((Y3 -' 1) mod (len u1)) + 1))} is non empty trivial finite 1 -element set
{{(u1 . (((Y3 -' 1) mod (len u1)) + 1)),(y . (((Y3 -' 1) div (len u1)) + 1))},{(u1 . (((Y3 -' 1) mod (len u1)) + 1))}} is non empty finite V31() set
Y2 . Y3 is set
card u 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
x is set
Y3 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
dom Y3 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
y is set
Y3 . x is set
Y3 . y is set
len Y3 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (len Y3) is finite len Y3 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Y3 ) } is set
Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 . Y33 is set
Y33 -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Y33 -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y33 -' 1) mod (len u1)) + 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
u1 . (((Y33 -' 1) mod (len u1)) + 1) is set
(Y33 -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y33 -' 1) div (len u1)) + 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
y . (((Y33 -' 1) div (len u1)) + 1) is set
[(u1 . (((Y33 -' 1) mod (len u1)) + 1)),(y . (((Y33 -' 1) div (len u1)) + 1))] is set
{(u1 . (((Y33 -' 1) mod (len u1)) + 1)),(y . (((Y33 -' 1) div (len u1)) + 1))} is non empty finite set
{(u1 . (((Y33 -' 1) mod (len u1)) + 1))} is non empty trivial finite 1 -element set
{{(u1 . (((Y33 -' 1) mod (len u1)) + 1)),(y . (((Y33 -' 1) div (len u1)) + 1))},{(u1 . (((Y33 -' 1) mod (len u1)) + 1))}} is non empty finite V31() set
Q0 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 . Q0 is set
Q0 -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Q0 -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Q0 -' 1) mod (len u1)) + 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
u1 . (((Q0 -' 1) mod (len u1)) + 1) is set
(Q0 -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Q0 -' 1) div (len u1)) + 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
y . (((Q0 -' 1) div (len u1)) + 1) is set
[(u1 . (((Q0 -' 1) mod (len u1)) + 1)),(y . (((Q0 -' 1) div (len u1)) + 1))] is set
{(u1 . (((Q0 -' 1) mod (len u1)) + 1)),(y . (((Q0 -' 1) div (len u1)) + 1))} is non empty finite set
{(u1 . (((Q0 -' 1) mod (len u1)) + 1))} is non empty trivial finite 1 -element set
{{(u1 . (((Q0 -' 1) mod (len u1)) + 1)),(y . (((Q0 -' 1) div (len u1)) + 1))},{(u1 . (((Q0 -' 1) mod (len u1)) + 1))}} is non empty finite V31() set
pp1 is set
u1 . pp1 is set
(len u1) * ((Y33 -' 1) div (len u1)) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((len u1) * ((Y33 -' 1) div (len u1))) + ((Y33 -' 1) mod (len u1)) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Y33 -' 1) + 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
Y33 + 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
(Y33 + 1) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Q0 -' 1) + 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
Q0 + 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
(Q0 + 1) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng Y3 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
x is set
y is set
Y33 is set
[y,Y33] is set
{y,Y33} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,Y33},{y}} is non empty finite V31() set
Q0 is set
u1 . Q0 is set
pp2 is set
y . pp2 is set
Seg (len y) is finite len y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len y ) } is set
pp1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
pp1 - 1 is ext-real V38() V39() V104() V161() Element of INT
x - 1 is ext-real V38() V39() V104() V161() Element of INT
P is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
nx is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len u1) * nx is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
P + ((len u1) * nx) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len u1) - 1 is ext-real V38() V39() V104() V161() Element of INT
(P + ((len u1) * nx)) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
P div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(P div (len u1)) + nx is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
0 + nx is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(P + ((len u1) * nx)) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
P mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(P + ((len u1) * nx)) + 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
((P + ((len u1) * nx)) + 1) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((P + ((len u1) * nx)) + 1) - 1 is ext-real V38() V39() V104() V161() Element of INT
(((P + ((len u1) * nx)) + 1) -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((((P + ((len u1) * nx)) + 1) -' 1) mod (len u1)) + 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
(((P + ((len u1) * nx)) + 1) -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((((P + ((len u1) * nx)) + 1) -' 1) div (len u1)) + 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
P + 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
(P + 1) + ((len u1) * nx) 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
(len u1) + ((len u1) * nx) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len y) - 1 is ext-real V38() V39() V104() V161() Element of INT
(len u1) * ((len y) - 1) is ext-real V38() V39() V104() V161() Element of INT
(len u1) + ((len u1) * ((len y) - 1)) is ext-real V38() V39() V104() V161() Element of INT
(len u1) * (len y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (len Y2) is finite len Y2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Y2 ) } is set
Y3 . ((P + ((len u1) * nx)) + 1) is set
x is set
y is set
Y3 . y is set
Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y33 -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Y33 -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y33 -' 1) mod (len u1)) + 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
u1 . (((Y33 -' 1) mod (len u1)) + 1) is set
(Y33 -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((Y33 -' 1) div (len u1)) + 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
y . (((Y33 -' 1) div (len u1)) + 1) is set
[(u1 . (((Y33 -' 1) mod (len u1)) + 1)),(y . (((Y33 -' 1) div (len u1)) + 1))] is set
{(u1 . (((Y33 -' 1) mod (len u1)) + 1)),(y . (((Y33 -' 1) div (len u1)) + 1))} is non empty finite set
{(u1 . (((Y33 -' 1) mod (len u1)) + 1))} is non empty trivial finite 1 -element set
{{(u1 . (((Y33 -' 1) mod (len u1)) + 1)),(y . (((Y33 -' 1) div (len u1)) + 1))},{(u1 . (((Y33 -' 1) mod (len u1)) + 1))}} is non empty finite V31() set
(len u1) * y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 | ((len u1) * y) is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
Seg ((len u1) * y) is finite (len u1) * y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= (len u1) * y ) } is set
Y3 | (Seg ((len u1) * y)) is Relation-like NAT -defined Seg ((len u1) * y) -defined NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSubsequence-like set
(len u1) * (len y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
len (Y3 | ((len u1) * y)) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 /^ ((len u1) * y) is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
Y33 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
Q0 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
Y33 ^ Q0 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
y | y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
Seg y is finite y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= y ) } is set
y | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Sigma -valued Function-like finite FinSubsequence-like set
pp2 is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len pp2 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 pp2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
rng pp2 is finite Element of bool Sigma
rng Y33 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
x is non empty finite Element of bool Sigma
[:u,x:] is Relation-like non empty finite set
P is set
nx is set
n1 is set
[nx,n1] is set
{nx,n1} is non empty finite set
{nx} is non empty trivial finite 1 -element set
{{nx,n1},{nx}} is non empty finite V31() set
n1 is set
u1 . n1 is set
n2 is set
pp2 . n2 is set
Seg (len pp2) is finite len pp2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len pp2 ) } is set
n2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
y . n2 is set
n1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
n1 - 1 is ext-real V38() V39() V104() V161() Element of INT
n2 - 1 is ext-real V38() V39() V104() V161() Element of INT
n11 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
n21 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len u1) * n21 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
n11 + ((len u1) * n21) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len u1) - 1 is ext-real V38() V39() V104() V161() Element of INT
(n11 + ((len u1) * n21)) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
n11 div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(n11 div (len u1)) + n21 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
0 + n21 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(n11 + ((len u1) * n21)) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
n11 mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(n11 + ((len u1) * n21)) + 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
((n11 + ((len u1) * n21)) + 1) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((n11 + ((len u1) * n21)) + 1) - 1 is ext-real V38() V39() V104() V161() Element of INT
(((n11 + ((len u1) * n21)) + 1) -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((((n11 + ((len u1) * n21)) + 1) -' 1) mod (len u1)) + 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
(((n11 + ((len u1) * n21)) + 1) -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((((n11 + ((len u1) * n21)) + 1) -' 1) div (len u1)) + 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
n11 + 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
(n11 + 1) + ((len u1) * n21) 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
(len u1) + ((len u1) * n21) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len pp2) - 1 is ext-real V38() V39() V104() V161() Element of INT
(len u1) * ((len pp2) - 1) is ext-real V38() V39() V104() V161() Element of INT
(len u1) + ((len u1) * ((len pp2) - 1)) is ext-real V38() V39() V104() V161() Element of INT
len Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (len Y33) is finite len Y33 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Y33 ) } is set
dom Y33 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Y33 . ((n11 + ((len u1) * n21)) + 1) is set
Y3 . ((n11 + ((len u1) * n21)) + 1) is set
P is set
nx is set
Y33 . nx is set
n1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 . n1 is set
n1 -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(n1 -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((n1 -' 1) mod (len u1)) + 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
u1 . (((n1 -' 1) mod (len u1)) + 1) is set
(n1 -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((n1 -' 1) div (len u1)) + 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
y . (((n1 -' 1) div (len u1)) + 1) is set
[(u1 . (((n1 -' 1) mod (len u1)) + 1)),(y . (((n1 -' 1) div (len u1)) + 1))] is set
{(u1 . (((n1 -' 1) mod (len u1)) + 1)),(y . (((n1 -' 1) div (len u1)) + 1))} is non empty finite set
{(u1 . (((n1 -' 1) mod (len u1)) + 1))} is non empty trivial finite 1 -element set
{{(u1 . (((n1 -' 1) mod (len u1)) + 1)),(y . (((n1 -' 1) div (len u1)) + 1))},{(u1 . (((n1 -' 1) mod (len u1)) + 1))}} is non empty finite V31() set
((len u1) * y) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((len u1) * y) -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((len u1) * y) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((len u1) * y) div (len u1)) - 1 is ext-real V38() V39() V104() V161() Element of INT
y - 1 is ext-real V38() V39() V104() V161() Element of INT
(y - 1) + 1 is ext-real V38() V39() V104() V161() Element of INT
Seg (len y) is finite len y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len y ) } is set
pp2 . (((n1 -' 1) div (len u1)) + 1) is set
P is set
nx is set
g . (P,nx) is set
[P,nx] is set
{P,nx} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,nx},{P}} is non empty finite V31() set
g . [P,nx] is ext-real V38() V39() set
v . P is ext-real V38() V39() Element of REAL
v1 . nx is ext-real V38() V39() Element of REAL
(v . P) * (v1 . nx) is ext-real V38() V39() Element of REAL
Func_Seq (g,Y33) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Y33 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,Y33)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,Y33)) is ext-real V38() V39() Element of REAL
Func_Seq (v1,pp2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
pp2 (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,pp2)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,pp2)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,pp2))) is ext-real V38() V39() Element of REAL
dom v is non empty Element of bool Omega
v * u1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (v * u1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom g is Relation-like Omega -defined Sigma -valued non empty Element of bool [:Omega,Sigma:]
y * (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(y * (len u1)) + (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
len Q0 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len Y3) - ((len u1) * y) is ext-real V38() V39() V104() V161() Element of INT
rng Q0 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
g * Q0 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (g * Q0) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom Q0 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
(Func_Seq (v1,y)) /. (y + 1) is ext-real V38() V39() Element of REAL
((Func_Seq (v1,y)) /. (y + 1)) (#) (v * u1) is Relation-like NAT -defined REAL -valued Function-like V146() V147() V148() Element of bool [:NAT,REAL:]
dom (((Func_Seq (v1,y)) /. (y + 1)) (#) (v * u1)) is V139() V140() V141() V142() V143() V144() Element of bool NAT
P is set
Seg (len Q0) is finite len Q0 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Q0 ) } is set
nx is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u1 /. nx is Element of Omega
u1 . nx is set
Seg (len y) is finite len y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len y ) } is set
y /. (y + 1) is Element of Sigma
y . (y + 1) is set
dom v1 is non empty Element of bool Sigma
v1 * y is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (v1 * y) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
v1 . (y /. (y + 1)) is ext-real V38() V39() Element of REAL
(v1 * y) . (y + 1) is ext-real V38() V39() Element of REAL
nx + ((len u1) * y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len u1) + ((len u1) * y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 . (nx + ((len u1) * y)) is set
(nx + ((len u1) * y)) -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((nx + ((len u1) * y)) -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((nx + ((len u1) * y)) -' 1) mod (len u1)) + 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
u1 . ((((nx + ((len u1) * y)) -' 1) mod (len u1)) + 1) is set
((nx + ((len u1) * y)) -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((nx + ((len u1) * y)) -' 1) div (len u1)) + 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
y . ((((nx + ((len u1) * y)) -' 1) div (len u1)) + 1) is set
[(u1 . ((((nx + ((len u1) * y)) -' 1) mod (len u1)) + 1)),(y . ((((nx + ((len u1) * y)) -' 1) div (len u1)) + 1))] is set
{(u1 . ((((nx + ((len u1) * y)) -' 1) mod (len u1)) + 1)),(y . ((((nx + ((len u1) * y)) -' 1) div (len u1)) + 1))} is non empty finite set
{(u1 . ((((nx + ((len u1) * y)) -' 1) mod (len u1)) + 1))} is non empty trivial finite 1 -element set
{{(u1 . ((((nx + ((len u1) * y)) -' 1) mod (len u1)) + 1)),(y . ((((nx + ((len u1) * y)) -' 1) div (len u1)) + 1))},{(u1 . ((((nx + ((len u1) * y)) -' 1) mod (len u1)) + 1))}} is non empty finite V31() set
(nx + ((len u1) * y)) - 1 is ext-real V38() V39() V104() V161() Element of INT
nx - 1 is ext-real V38() V39() V104() V161() Element of INT
(nx - 1) + ((len u1) * y) is ext-real V38() V39() V104() V161() Element of INT
nx -' 1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(nx -' 1) + ((len u1) * y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((nx -' 1) + ((len u1) * y)) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((nx -' 1) + ((len u1) * y)) div (len u1)) + 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
(nx -' 1) div (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((nx -' 1) div (len u1)) + y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((nx -' 1) div (len u1)) + y) + 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
0 + y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(0 + y) + 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
((nx -' 1) + ((len u1) * y)) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(((nx -' 1) + ((len u1) * y)) mod (len u1)) + 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
(nx -' 1) mod (len u1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
((nx -' 1) mod (len u1)) + 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
(nx -' 1) + 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
(nx - 1) + 1 is ext-real V38() V39() V104() V161() Element of INT
Q0 . nx is set
[(u1 /. nx),(y /. (y + 1))] is set
{(u1 /. nx),(y /. (y + 1))} is non empty finite set
{(u1 /. nx)} is non empty trivial finite 1 -element set
{{(u1 /. nx),(y /. (y + 1))},{(u1 /. nx)}} is non empty finite V31() set
(g * Q0) . P is ext-real V38() V39() Element of REAL
g . ((u1 /. nx),(y /. (y + 1))) is ext-real V38() V39() Element of REAL
g . [(u1 /. nx),(y /. (y + 1))] is ext-real V38() V39() set
v . (u1 /. nx) is ext-real V38() V39() Element of REAL
(v . (u1 /. nx)) * (v1 . (y /. (y + 1))) is ext-real V38() V39() Element of REAL
(v * u1) . nx is ext-real V38() V39() Element of REAL
((v * u1) . nx) * ((Func_Seq (v1,y)) /. (y + 1)) is ext-real V38() V39() Element of REAL
(((Func_Seq (v1,y)) /. (y + 1)) (#) (v * u1)) . P is ext-real V38() V39() Element of REAL
Func_Seq (g,Q0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Q0 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
((Func_Seq (v1,y)) /. (y + 1)) * (Func_Seq (v,u1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
((Func_Seq (v1,y)) /. (y + 1)) multreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:REAL,REAL:]
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() V222( REAL ) V223( REAL ) V247( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total V146() V147() V148() V150() V152() Element of bool [:REAL,REAL:]
multreal [;] (((Func_Seq (v1,y)) /. (y + 1)),(id REAL)) is set
(Func_Seq (v,u1)) (#) (((Func_Seq (v1,y)) /. (y + 1)) multreal) is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,Q0)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,Q0)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * ((Func_Seq (v1,y)) /. (y + 1)) is ext-real V38() V39() Element of REAL
Func_Seq (g,Y3) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Y3 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
(Func_Seq (g,Y33)) ^ (Func_Seq (g,Q0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
dom (Func_Seq (v1,y)) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
len (Func_Seq (v1,y)) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(Func_Seq (v1,y)) | y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
(Func_Seq (v1,y)) | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V146() V147() V148() set
<*((Func_Seq (v1,y)) /. (y + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V146() V147() V148() V150() V151() V152() V153() FinSequence of REAL
[1,((Func_Seq (v1,y)) /. (y + 1))] is set
{1,((Func_Seq (v1,y)) /. (y + 1))} is non empty finite V139() V140() V141() set
{{1,((Func_Seq (v1,y)) /. (y + 1))},{1}} is non empty finite V31() set
{[1,((Func_Seq (v1,y)) /. (y + 1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(Func_Seq (v1,pp2)) ^ <*((Func_Seq (v1,y)) /. (y + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Sum (Func_Seq (g,Y3)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,Y3)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (g,Y33))) + (Sum (Func_Seq (g,Q0))) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v1,pp2))) + ((Func_Seq (v1,y)) /. (y + 1)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * ((Sum (Func_Seq (v1,pp2))) + ((Func_Seq (v1,y)) /. (y + 1))) is ext-real V38() V39() Element of REAL
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
dom s1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
[:(dom s1),(dom s1):] is Relation-like RAT -valued INT -valued finite V146() V147() V148() V149() set
bool [:(dom s1),(dom s1):] is non empty finite V31() set
P is Relation-like dom s1 -defined dom s1 -valued Function-like one-to-one finite total quasi_total onto bijective V146() V147() V148() V149() Element of bool [:(dom s1),(dom s1):]
s1 * P is Relation-like dom s1 -defined [:Omega,Sigma:] -valued Function-like finite Element of bool [:(dom s1),[:Omega,Sigma:]:]
[:(dom s1),[:Omega,Sigma:]:] is Relation-like set
bool [:(dom s1),[:Omega,Sigma:]:] is non empty set
dom P is finite V139() V140() V141() V142() V143() V144() Element of bool (dom s1)
bool (dom s1) is non empty finite V31() set
rng P is finite V139() V140() V141() V142() V143() V144() Element of bool REAL
Func_Seq (g,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s1 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
(Func_Seq (g,s1)) * P is Relation-like dom s1 -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:(dom s1),REAL:]
[:(dom s1),REAL:] is Relation-like V146() V147() V148() set
bool [:(dom s1),REAL:] is non empty set
dom (Func_Seq (g,s1)) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng y is finite Element of bool Sigma
Y1 is non empty finite Element of bool Sigma
s1 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng s1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
f2 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
[:u,Y1:] is Relation-like non empty finite set
Func_Seq (g,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s1 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
rng y is finite Element of bool Sigma
Y1 is non empty finite Element of bool Sigma
s1 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng s1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
f2 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
[:u,Y1:] is Relation-like non empty finite set
Func_Seq (g,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s1 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
rng y is finite Element of bool Sigma
s1 is non empty finite Element of bool Sigma
y is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng y is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
Y1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
[:u,s1:] is Relation-like non empty finite set
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Func_Seq (g,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
rng y is finite Element of bool Sigma
s1 is non empty finite Element of bool Sigma
y is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng y is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
Y1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
[:u,s1:] is Relation-like non empty finite set
Func_Seq (g,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,y)) is ext-real V38() V39() Element of REAL
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (v,u1))) * (Sum (Func_Seq (v1,y))) 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 non empty set
[:Sigma,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Sigma,REAL:] is non empty non trivial non finite set
[:Omega,Sigma:] is Relation-like non empty 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
bool Omega is non empty set
bool Sigma is non empty set
bool [:Omega,Sigma:] is non empty set
v is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v1 is Relation-like Sigma -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Sigma,REAL:]
g is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
u is non empty finite Element of bool Omega
setopfunc (u,Omega,REAL,v,addreal) is ext-real V38() V39() Element of REAL
u1 is non empty finite Element of bool Sigma
[:u,u1:] is Relation-like non empty finite set
setopfunc (u1,Sigma,REAL,v1,addreal) is ext-real V38() V39() Element of REAL
(setopfunc (u,Omega,REAL,v,addreal)) * (setopfunc (u1,Sigma,REAL,v1,addreal)) is ext-real V38() V39() Element of REAL
h is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (h,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng y is finite Element of bool Omega
Func_Seq (v,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v,y)) is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
rng y is finite Element of bool Sigma
Func_Seq (v1,y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
y (#) v1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (v1,y)) is ext-real V38() V39() Element of REAL
s1 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
rng s1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
Func_Seq (g,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s1 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (g,s1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (g,s1)) 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
bool Omega is non empty set
Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v is finite Element of bool Omega
setopfunc (v,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
v1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng v1 is finite Element of bool Omega
Func_Seq (Sigma,v1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
v1 (#) Sigma is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (Sigma,v1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (Sigma,v1)) is ext-real V38() V39() Element of REAL
g is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
dom (Func_Seq (Sigma,v1)) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
(Func_Seq (Sigma,v1)) . g is ext-real V38() V39() Element of REAL
v1 . g is set
Sigma . (v1 . g) is ext-real V38() V39() Element of REAL
dom v1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
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
bool Omega is non empty set
Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v is finite Element of bool Omega
v1 is finite Element of bool Omega
setopfunc (v,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
setopfunc (v1,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
g is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng g is finite Element of bool Omega
Func_Seq (Sigma,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
g (#) Sigma is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (Sigma,g)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (Sigma,g)) is ext-real V38() V39() Element of REAL
v1 \ v is finite Element of bool Omega
u is finite Element of bool Omega
setopfunc (u,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
u1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng u1 is finite Element of bool Omega
Func_Seq (Sigma,u1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
u1 (#) Sigma is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (Sigma,u1)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (Sigma,u1)) is ext-real V38() V39() Element of REAL
h is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
dom (Func_Seq (Sigma,u1)) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
(Func_Seq (Sigma,u1)) . h is ext-real V38() V39() Element of REAL
u1 . h is set
Sigma . (u1 . h) is ext-real V38() V39() Element of REAL
dom u1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
g ^ u1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
h is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng h is finite Element of bool Omega
(rng g) \/ (rng u1) is finite Element of bool Omega
v \/ v1 is finite Element of bool Omega
Func_Seq (Sigma,h) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
h (#) Sigma is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Sum (Func_Seq (Sigma,h)) is ext-real V38() V39() Element of REAL
addreal "**" (Func_Seq (Sigma,h)) is ext-real V38() V39() Element of REAL
(Func_Seq (Sigma,g)) ^ (Func_Seq (Sigma,u1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
(Sum (Func_Seq (Sigma,g))) + 0 is ext-real V38() V39() Element of REAL
(Sum (Func_Seq (Sigma,g))) + (Sum (Func_Seq (Sigma,u1))) 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
[: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 Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
P2M Sigma is Relation-like Trivial-SigmaField Omega -defined ExtREAL -valued Function-like non empty finite total quasi_total V147() V155() nonnegative V204(Omega, Trivial-SigmaField Omega) Element of bool [:(Trivial-SigmaField Omega),ExtREAL:]
[:(Trivial-SigmaField Omega),ExtREAL:] is Relation-like non empty V147() set
bool [:(Trivial-SigmaField Omega),ExtREAL:] is non empty set
v is non empty finite Element of bool Omega
card v 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
v1 is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v1 | v is Relation-like Omega -defined v -defined Omega -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M Sigma),(v1 | v)) is ext-real Element of ExtREAL
Omega \ v is finite Element of bool Omega
(Omega \ v) --> 0 is Relation-like Omega \ v -defined NAT -valued RAT -valued INT -valued Function-like finite total quasi_total V146() V147() V148() V149() Element of bool [:(Omega \ v),NAT:]
[:(Omega \ v),NAT:] is Relation-like RAT -valued INT -valued V146() V147() V148() V149() set
bool [:(Omega \ v),NAT:] is non empty set
dom ((Omega \ v) --> 0) is finite Element of bool (Omega \ v)
bool (Omega \ v) is non empty finite V31() set
rng ((Omega \ v) --> 0) is finite V139() V140() V141() V142() V143() V144() Element of bool REAL
v1 +* ((Omega \ v) --> 0) is Relation-like Function-like finite V146() V147() V148() set
dom (v1 +* ((Omega \ v) --> 0)) is finite set
dom v1 is non empty finite Element of bool Omega
(dom v1) \/ (dom ((Omega \ v) --> 0)) is non empty finite set
Omega \/ (Omega \ v) is non empty finite set
rng (v1 +* ((Omega \ v) --> 0)) is finite V139() V140() V141() Element of bool REAL
card Omega 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
u is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M Sigma),u) is ext-real Element of ExtREAL
u1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
len u1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
h is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng h is finite Element of bool Omega
len h 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 u1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum u1 is ext-real V38() V39() Element of REAL
addreal "**" u1 is ext-real V38() V39() Element of REAL
y is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Trivial-SigmaField Omega
dom y is non empty finite Element of bool Omega
v \/ (Omega \ v) is non empty finite Element of bool Omega
y | (v \/ (Omega \ v)) is Relation-like Omega -defined v \/ (Omega \ v) -defined Omega -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M Sigma),(y | (v \/ (Omega \ v)))) is ext-real Element of ExtREAL
y | v is Relation-like Omega -defined v -defined Omega -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M Sigma),(y | v)) is ext-real Element of ExtREAL
y | (Omega \ v) is Relation-like Omega -defined Omega \ v -defined Omega -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M Sigma),(y | (Omega \ v))) is ext-real Element of ExtREAL
(Integral ((P2M Sigma),(y | v))) + (Integral ((P2M Sigma),(y | (Omega \ v)))) is ext-real Element of ExtREAL
v \/ Omega is non empty finite set
dom (y | (Omega \ v)) is finite Element of bool Omega
y is set
(y | (Omega \ v)) . y is ext-real V38() V39() Element of REAL
y . y is ext-real V38() V39() Element of REAL
((Omega \ v) --> 0) . y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
R_EAL 0 is ext-real Element of ExtREAL
(P2M Sigma) . (Omega \ v) is ext-real Element of ExtREAL
(R_EAL 0) * ((P2M Sigma) . (Omega \ v)) is ext-real Element of ExtREAL
Integral ((P2M Sigma),y) is ext-real Element of ExtREAL
h " v is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom h is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
[:(dom h),(rng h):] is Relation-like finite set
bool [:(dom h),(rng h):] is non empty finite V31() set
bool (dom h) is non empty finite V31() set
Seg (len u1) is finite len u1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len u1 ) } is set
bool (Seg (len u1)) is non empty finite V31() set
s1 is finite V139() V140() V141() V142() V143() V144() Element of bool (Seg (len u1))
canFS s1 is Relation-like NAT -defined s1 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like onto bijective V146() V147() V148() V149() FinSequence of s1
rng (canFS s1) is finite V139() V140() V141() V142() V143() V144() Element of bool REAL
[:(Seg (len u1)),Omega:] is Relation-like finite set
bool [:(Seg (len u1)),Omega:] is non empty finite V31() set
h * (canFS s1) is Relation-like NAT -defined Omega -valued Function-like finite Element of bool [:NAT,Omega:]
[:NAT,Omega:] is Relation-like non empty non trivial non finite set
bool [:NAT,Omega:] is non empty non trivial non finite set
Y1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng Y1 is finite Element of bool Omega
h .: (rng (canFS s1)) is finite Element of bool Omega
h .: s1 is finite Element of bool Omega
(Seg (len u1)) \ s1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
G2 is finite V139() V140() V141() V142() V143() V144() Element of bool (Seg (len u1))
canFS G2 is Relation-like NAT -defined G2 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like onto bijective V146() V147() V148() V149() FinSequence of G2
rng (canFS G2) is finite V139() V140() V141() V142() V143() V144() Element of bool REAL
h * (canFS G2) is Relation-like NAT -defined Omega -valued Function-like finite Element of bool [:NAT,Omega:]
s2 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
Y1 ^ s2 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
h | s1 is Relation-like NAT -defined s1 -defined NAT -defined Omega -valued Function-like finite FinSubsequence-like Element of bool [:NAT,Omega:]
rng (h | s1) is finite Element of bool Omega
h | G2 is Relation-like NAT -defined G2 -defined NAT -defined Omega -valued Function-like finite FinSubsequence-like Element of bool [:NAT,Omega:]
rng (h | G2) is finite Element of bool Omega
rng s2 is finite Element of bool Omega
Y2 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
len (canFS s1) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
card s1 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 (canFS s1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (card s1) is finite card s1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= card s1 ) } is set
dom Y1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
len Y1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
len (canFS G2) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
card G2 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 (canFS G2) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (card G2) is finite card G2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= card G2 ) } is set
dom s2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
len s2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
s1 \/ G2 is finite V139() V140() V141() V142() V143() V144() Element of bool (Seg (len u1))
(Seg (len u1)) \/ s1 is finite V139() V140() V141() V142() V143() V144() set
dom Y2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
(len Y1) + (len s2) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg ((len Y1) + (len s2)) is finite (len Y1) + (len s2) -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= (len Y1) + (len s2) ) } is set
card (s1 \/ G2) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (card (s1 \/ G2)) is finite card (s1 \/ G2) -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= card (s1 \/ G2) ) } is set
len Y2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Seg (len h) is finite len h -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len h ) } is set
Seg (len Y2) is finite len Y2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Y2 ) } is set
card (dom Y2) 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 Y2),Omega:] is Relation-like finite set
bool [:(dom Y2),Omega:] is non empty finite V31() set
rng Y2 is finite Element of bool Omega
[:(dom h),(dom h):] is Relation-like RAT -valued INT -valued finite V146() V147() V148() V149() set
bool [:(dom h),(dom h):] is non empty finite V31() set
Y3 is Relation-like dom h -defined dom h -valued Function-like one-to-one finite total quasi_total onto bijective V146() V147() V148() V149() Element of bool [:(dom h),(dom h):]
h * Y3 is Relation-like dom h -defined Omega -valued Function-like finite Element of bool [:(dom h),Omega:]
[:(dom h),Omega:] is Relation-like finite set
bool [:(dom h),Omega:] is non empty finite V31() set
dom Y3 is finite V139() V140() V141() V142() V143() V144() Element of bool (dom h)
rng Y3 is finite V139() V140() V141() V142() V143() V144() Element of bool REAL
x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
Seg (card Omega) is non empty finite card Omega -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= card Omega ) } is set
Y2 . x is set
v1 . (Y2 . x) is ext-real V38() V39() Element of REAL
{(Y2 . x)} is non empty trivial finite 1 -element set
Sigma . {(Y2 . x)} is ext-real V38() V39() Element of REAL
(v1 . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
y . (Y2 . x) is ext-real V38() V39() Element of REAL
(y . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
Y2 . x is set
v1 . (Y2 . x) is ext-real V38() V39() Element of REAL
{(Y2 . x)} is non empty trivial finite 1 -element set
Sigma . {(Y2 . x)} is ext-real V38() V39() Element of REAL
(v1 . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
y . (Y2 . x) is ext-real V38() V39() Element of REAL
(y . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
Y2 . x is set
v1 . (Y2 . x) is ext-real V38() V39() Element of REAL
{(Y2 . x)} is non empty trivial finite 1 -element set
Sigma . {(Y2 . x)} is ext-real V38() V39() Element of REAL
(v1 . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
y . (Y2 . x) is ext-real V38() V39() Element of REAL
(y . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
Y2 . x is set
v1 . (Y2 . x) is ext-real V38() V39() Element of REAL
{(Y2 . x)} is non empty trivial finite 1 -element set
Sigma . {(Y2 . x)} is ext-real V38() V39() Element of REAL
(v1 . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
y . (Y2 . x) is ext-real V38() V39() Element of REAL
(y . (Y2 . x)) * (Sigma . {(Y2 . x)}) is ext-real V38() V39() Element of REAL
y is ext-real V38() V39() Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
dom x is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
u1 * Y3 is Relation-like dom h -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:(dom h),REAL:]
[:(dom h),REAL:] is Relation-like V146() V147() V148() set
bool [:(dom h),REAL:] is non empty set
dom (u1 * Y3) is finite V139() V140() V141() V142() V143() V144() Element of bool (dom h)
y is set
Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y2 . Y33 is set
Y3 . Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() Element of REAL
h . (Y3 . Y33) is set
u1 . (Y3 . Y33) is ext-real V38() V39() Element of REAL
y . (h . (Y3 . Y33)) is ext-real V38() V39() Element of REAL
{(h . (Y3 . Y33))} is non empty trivial finite 1 -element set
Sigma . {(h . (Y3 . Y33))} is ext-real V38() V39() Element of REAL
(y . (h . (Y3 . Y33))) * (Sigma . {(h . (Y3 . Y33))}) is ext-real V38() V39() Element of REAL
x . Y33 is ext-real V38() V39() Element of REAL
v1 . (Y2 . Y33) is ext-real V38() V39() Element of REAL
{(Y2 . Y33)} is non empty trivial finite 1 -element set
Sigma . {(Y2 . Y33)} is ext-real V38() V39() Element of REAL
(v1 . (Y2 . Y33)) * (Sigma . {(Y2 . Y33)}) is ext-real V38() V39() Element of REAL
(v1 | v) . (h . (Y3 . Y33)) is ext-real V38() V39() Element of REAL
((v1 | v) . (h . (Y3 . Y33))) * (Sigma . {(h . (Y3 . Y33))}) is ext-real V38() V39() Element of REAL
(u1 * Y3) . Y33 is ext-real V38() V39() Element of REAL
x . Y33 is ext-real V38() V39() Element of REAL
(u1 * Y3) . Y33 is ext-real V38() V39() Element of REAL
x . Y33 is ext-real V38() V39() Element of REAL
(u1 * Y3) . Y33 is ext-real V38() V39() Element of REAL
x . Y33 is ext-real V38() V39() Element of REAL
(u1 * Y3) . Y33 is ext-real V38() V39() Element of REAL
x . y is ext-real V38() V39() Element of REAL
(u1 * Y3) . y is ext-real V38() V39() Element of REAL
Sum x is ext-real V38() V39() Element of REAL
addreal "**" x is ext-real V38() V39() Element of REAL
y is Relation-like NAT -defined v -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of v
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
x | (len y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Seg (len y) is finite len y -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len y ) } is set
x | (Seg (len y)) is Relation-like NAT -defined Seg (len y) -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V146() V147() V148() set
x /^ (len y) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Y33 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Q0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Y33 ^ Q0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
len x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len y) + (len s2) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
len Q0 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
(len x) - (len y) is ext-real V38() V39() V104() V161() Element of INT
dom Q0 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len s2) is finite len s2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len s2 ) } is set
(len s2) |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() V149() Element of (len s2) -tuples_on NAT
(len s2) -tuples_on NAT is FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = len s2 } is set
(Seg (len s2)) --> 0 is Relation-like Seg (len s2) -defined RAT -valued INT -valued {0} -valued Function-like finite total quasi_total V146() V147() V148() V149() Element of bool [:(Seg (len s2)),{0}:]
{0} is functional non empty trivial finite V31() 1 -element V139() V140() V141() V142() V143() V144() set
[:(Seg (len s2)),{0}:] is Relation-like RAT -valued INT -valued finite V146() V147() V148() V149() set
bool [:(Seg (len s2)),{0}:] is non empty finite V31() set
dom ((len s2) |-> 0) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
pp1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
pp1 + (len y) is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y2 . (pp1 + (len y)) is set
s2 . pp1 is set
rng y is finite Element of bool v
bool v is non empty finite V31() set
(rng y) /\ (rng s2) is finite Element of bool Omega
y . (s2 . pp1) is ext-real V38() V39() Element of REAL
(y | (Omega \ v)) . (s2 . pp1) is ext-real V38() V39() Element of REAL
x . (pp1 + (len y)) is ext-real V38() V39() Element of REAL
y . (Y2 . (pp1 + (len y))) is ext-real V38() V39() Element of REAL
{(Y2 . (pp1 + (len y)))} is non empty trivial finite 1 -element set
Sigma . {(Y2 . (pp1 + (len y)))} is ext-real V38() V39() Element of REAL
(y . (Y2 . (pp1 + (len y)))) * (Sigma . {(Y2 . (pp1 + (len y)))}) is ext-real V38() V39() Element of REAL
Q0 . pp1 is ext-real V38() V39() Element of REAL
((len s2) |-> 0) . pp1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() Element of REAL
Sum Y33 is ext-real V38() V39() Element of REAL
addreal "**" Y33 is ext-real V38() V39() Element of REAL
Sum Q0 is ext-real V38() V39() Element of REAL
addreal "**" Q0 is ext-real V38() V39() Element of REAL
(Sum Y33) + (Sum Q0) is ext-real V38() V39() Element of REAL
(Sum Y33) + 0 is ext-real V38() V39() Element of REAL
len Y33 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 Y33 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
pp1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() set
Y33 . pp1 is ext-real V38() V39() Element of REAL
y . pp1 is set
v1 . (y . pp1) is ext-real V38() V39() Element of REAL
{(y . pp1)} is non empty trivial finite 1 -element set
Sigma . {(y . pp1)} is ext-real V38() V39() Element of REAL
(v1 . (y . pp1)) * (Sigma . {(y . pp1)}) is ext-real V38() V39() Element of REAL
dom y is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Y2 . pp1 is set
x . pp1 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
bool [:Omega,Sigma:] is non empty finite V31() set
[:(bool [:Omega,Sigma:]),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(bool [:Omega,Sigma:]),REAL:] is non empty non trivial non finite set
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
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 bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
u1 is non empty finite Element of bool Omega
v . u1 is ext-real V38() V39() Element of REAL
h is non empty finite Element of bool Sigma
[:u1,h:] is Relation-like non empty finite set
u . [:u1,h:] is ext-real V38() V39() Element of REAL
v1 . h is ext-real V38() V39() Element of REAL
(v . u1) * (v1 . h) is ext-real V38() V39() Element of REAL
y is set
{y} is non empty trivial finite 1 -element set
v . {y} is ext-real V38() V39() Element of REAL
[:u1,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:u1,REAL:] is non empty non trivial non finite set
y is Relation-like u1 -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:u1,REAL:]
y is set
{y} is non empty trivial finite 1 -element set
v1 . {y} is ext-real V38() V39() Element of REAL
[:h,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:h,REAL:] is non empty non trivial non finite set
y is Relation-like h -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:h,REAL:]
s1 is set
chi (u1,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 (u1,Omega)) is finite Element of bool Omega
rng (chi (u1,Omega)) is V140() Element of bool ExtREAL
[:Omega,{{},1}:] is Relation-like RAT -valued INT -valued non empty finite V146() V147() V148() V149() set
bool [:Omega,{{},1}:] is non empty finite V31() 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
s1 is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
s1 | u1 is Relation-like Omega -defined u1 -defined Omega -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:Omega,REAL:]
dom (s1 | u1) is finite Element of bool Omega
dom s1 is non empty finite Element of bool Omega
(dom s1) /\ u1 is finite Element of bool Omega
Y1 is set
(s1 | u1) . Y1 is ext-real V38() V39() Element of REAL
s1 . Y1 is ext-real V38() V39() Element of REAL
P2M v is Relation-like Trivial-SigmaField Omega -defined ExtREAL -valued Function-like non empty finite total quasi_total V147() V155() nonnegative V204(Omega, Trivial-SigmaField Omega) Element of bool [:(Trivial-SigmaField Omega),ExtREAL:]
[:(Trivial-SigmaField Omega),ExtREAL:] is Relation-like non empty V147() set
bool [:(Trivial-SigmaField Omega),ExtREAL:] is non empty set
Integral ((P2M v),(s1 | u1)) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
(P2M v) . (dom (s1 | u1)) is ext-real Element of ExtREAL
(R_EAL 1) * ((P2M v) . (dom (s1 | u1))) is ext-real Element of ExtREAL
1 * (v . u1) is ext-real V38() V39() Element of REAL
card u1 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
Y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
len Y1 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
f2 is Relation-like NAT -defined u1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of u1
rng f2 is finite Element of bool u1
bool u1 is non empty finite V31() set
len f2 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 Y1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum Y1 is ext-real V38() V39() Element of REAL
addreal "**" Y1 is ext-real V38() V39() Element of REAL
dom y is non empty finite Element of bool u1
y * f2 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (y * f2) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom f2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len f2) is finite len f2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len f2 ) } is set
s2 is set
Y2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
f2 . Y2 is set
Y1 . s2 is ext-real V38() V39() Element of REAL
s1 . (f2 . Y2) is ext-real V38() V39() Element of REAL
{(f2 . Y2)} is non empty trivial finite 1 -element set
v . {(f2 . Y2)} is ext-real V38() V39() Element of REAL
(s1 . (f2 . Y2)) * (v . {(f2 . Y2)}) is ext-real V38() V39() Element of REAL
1 * (v . {(f2 . Y2)}) is ext-real V38() V39() Element of REAL
y . (f2 . Y2) is ext-real V38() V39() Element of REAL
(y * f2) . s2 is ext-real V38() V39() Element of REAL
Func_Seq (y,f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
f2 (#) y is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
G2 is finite Element of bool u1
setopfunc (G2,u1,REAL,y,addreal) is ext-real V38() V39() Element of REAL
chi (h,Sigma) is Relation-like Sigma -defined ExtREAL -valued Function-like V147() Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is Relation-like non empty V147() set
bool [:Sigma,ExtREAL:] is non empty set
dom (chi (h,Sigma)) is finite Element of bool Sigma
rng (chi (h,Sigma)) is V140() Element of bool ExtREAL
[:Sigma,{{},1}:] is Relation-like RAT -valued INT -valued non empty finite V146() V147() V148() V149() set
bool [:Sigma,{{},1}:] is non empty finite V31() set
[:Sigma,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Sigma,REAL:] is non empty non trivial non finite set
s2 is Relation-like Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Sigma,REAL:]
s2 | h is Relation-like Sigma -defined h -defined Sigma -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:Sigma,REAL:]
dom (s2 | h) is finite Element of bool Sigma
dom s2 is non empty finite Element of bool Sigma
(dom s2) /\ h is finite Element of bool Sigma
Y2 is set
(s2 | h) . Y2 is ext-real V38() V39() Element of REAL
s2 . Y2 is ext-real V38() V39() Element of REAL
P2M v1 is Relation-like Trivial-SigmaField Sigma -defined ExtREAL -valued Function-like non empty finite total quasi_total V147() V155() nonnegative V204(Sigma, Trivial-SigmaField Sigma) Element of bool [:(Trivial-SigmaField Sigma),ExtREAL:]
[:(Trivial-SigmaField Sigma),ExtREAL:] is Relation-like non empty V147() set
bool [:(Trivial-SigmaField Sigma),ExtREAL:] is non empty set
Integral ((P2M v1),(s2 | h)) is ext-real Element of ExtREAL
(P2M v1) . h is ext-real Element of ExtREAL
(R_EAL 1) * ((P2M v1) . h) is ext-real Element of ExtREAL
1 * (v1 . h) is ext-real V38() V39() Element of REAL
card h 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
Y2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
len Y2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 is Relation-like NAT -defined h -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of h
rng Y3 is finite Element of bool h
bool h is non empty finite V31() set
len Y3 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 Y2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum Y2 is ext-real V38() V39() Element of REAL
addreal "**" Y2 is ext-real V38() V39() Element of REAL
dom y is non empty finite Element of bool h
y * Y3 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (y * Y3) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom Y3 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len Y3) is finite len Y3 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len Y3 ) } is set
y is set
Y33 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
Y3 . Y33 is set
Y2 . y is ext-real V38() V39() Element of REAL
s2 . (Y3 . Y33) is ext-real V38() V39() Element of REAL
{(Y3 . Y33)} is non empty trivial finite 1 -element set
v1 . {(Y3 . Y33)} is ext-real V38() V39() Element of REAL
(s2 . (Y3 . Y33)) * (v1 . {(Y3 . Y33)}) is ext-real V38() V39() Element of REAL
1 * (v1 . {(Y3 . Y33)}) is ext-real V38() V39() Element of REAL
y . (Y3 . Y33) is ext-real V38() V39() Element of REAL
(y * Y3) . y is ext-real V38() V39() Element of REAL
Func_Seq (y,Y3) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
Y3 (#) y is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
x is finite Element of bool h
setopfunc (x,h,REAL,y,addreal) is ext-real V38() V39() Element of REAL
bool [:u1,h:] is non empty finite V31() set
[:[:u1,h:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:u1,h:],REAL:] is non empty non trivial non finite set
g | [:u1,h:] is Relation-like [:Omega,Sigma:] -defined [:u1,h:] -defined [:Omega,Sigma:] -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
pp1 is set
pp2 is set
[pp1,pp2] is set
{pp1,pp2} is non empty finite set
{pp1} is non empty trivial finite 1 -element set
{{pp1,pp2},{pp1}} is non empty finite V31() set
Q0 is Relation-like [:u1,h:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:u1,h:],REAL:]
dom Q0 is Relation-like u1 -defined h -valued non empty finite Element of bool [:u1,h:]
Q0 . (pp1,pp2) is set
Q0 . [pp1,pp2] is ext-real V38() V39() set
g . (pp1,pp2) is set
g . [pp1,pp2] is ext-real V38() V39() set
v . {pp1} is ext-real V38() V39() Element of REAL
{pp2} is non empty trivial finite 1 -element set
v1 . {pp2} is ext-real V38() V39() Element of REAL
(v . {pp1}) * (v1 . {pp2}) is ext-real V38() V39() Element of REAL
y . pp1 is ext-real V38() V39() Element of REAL
(y . pp1) * (v1 . {pp2}) is ext-real V38() V39() Element of REAL
y . pp2 is ext-real V38() V39() Element of REAL
(y . pp1) * (y . pp2) is ext-real V38() V39() Element of REAL
y is Relation-like u1 -defined h -valued finite Element of bool [:u1,h:]
setopfunc (y,[:u1,h:],REAL,Q0,addreal) is ext-real V38() V39() Element of REAL
pp1 is Relation-like NAT -defined [:u1,h:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:u1,h:]
rng pp1 is Relation-like u1 -defined h -valued finite Element of bool [:u1,h:]
Func_Seq (Q0,pp1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
pp1 (#) Q0 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
addreal "**" (Func_Seq (Q0,pp1)) is ext-real V38() V39() Element of REAL
dom g is Relation-like Omega -defined Sigma -valued non empty finite Element of bool [:Omega,Sigma:]
g * pp1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (g * pp1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom pp1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Q0 * pp1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (Q0 * pp1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
x is set
(Q0 * pp1) . x is ext-real V38() V39() Element of REAL
(g * pp1) . x is ext-real V38() V39() Element of REAL
pp1 . x is set
Q0 . (pp1 . x) is ext-real V38() V39() Element of REAL
g . (pp1 . x) is ext-real V38() V39() Element of REAL
pp2 is Relation-like NAT -defined [:Omega,Sigma:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:Omega,Sigma:]
Func_Seq (g,pp2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
pp2 (#) g is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
Y33 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (Y33,[:Omega,Sigma:],REAL,g,addreal) 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
bool [:Omega,Sigma:] is non empty finite V31() set
[:(bool [:Omega,Sigma:]),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(bool [:Omega,Sigma:]),REAL:] is non empty non trivial non finite set
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
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 bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
u . [:Omega,Sigma:] is ext-real V38() V39() Element of REAL
u1 is set
{u1} is non empty trivial finite 1 -element set
v . {u1} is ext-real V38() V39() Element of 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
u1 is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
h is set
{h} is non empty trivial finite 1 -element set
v1 . {h} is ext-real V38() V39() Element of REAL
[:Sigma,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Sigma,REAL:] is non empty non trivial non finite set
h is Relation-like Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Sigma,REAL:]
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty finite 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 finite Element of bool Omega
rng (Omega --> 1) is non empty finite V139() V140() V141() V142() V143() V144() Element of bool REAL
y is set
(Omega --> 1) . y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
P2M v is Relation-like Trivial-SigmaField Omega -defined ExtREAL -valued Function-like non empty finite total quasi_total V147() V155() nonnegative V204(Omega, Trivial-SigmaField Omega) Element of bool [:(Trivial-SigmaField Omega),ExtREAL:]
[:(Trivial-SigmaField Omega),ExtREAL:] is Relation-like non empty V147() set
bool [:(Trivial-SigmaField Omega),ExtREAL:] is non empty set
y is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M v),y) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
(P2M v) . Omega is ext-real Element of ExtREAL
(R_EAL 1) * ((P2M v) . Omega) is ext-real Element of ExtREAL
v . Omega is ext-real V38() V39() Element of REAL
1 * (v . Omega) is ext-real V38() V39() Element of REAL
card Omega 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
y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
len y is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
s1 is Relation-like NAT -defined Omega -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng s1 is finite Element of bool Omega
len s1 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 y is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum y is ext-real V38() V39() Element of REAL
addreal "**" y is ext-real V38() V39() Element of REAL
dom u1 is non empty finite Element of bool Omega
Y1 is finite Element of bool Omega
u1 * s1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (u1 * s1) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom s1 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len s1) is finite len s1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len s1 ) } is set
f2 is set
y . f2 is ext-real V38() V39() Element of REAL
G2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
s1 . G2 is set
y . (s1 . G2) is ext-real V38() V39() Element of REAL
{(s1 . G2)} is non empty trivial finite 1 -element set
v . {(s1 . G2)} is ext-real V38() V39() Element of REAL
(y . (s1 . G2)) * (v . {(s1 . G2)}) is ext-real V38() V39() Element of REAL
1 * (v . {(s1 . G2)}) is ext-real V38() V39() Element of REAL
u1 . (s1 . G2) is ext-real V38() V39() Element of REAL
(u1 * s1) . f2 is ext-real V38() V39() Element of REAL
Func_Seq (u1,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s1 (#) u1 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
setopfunc (Y1,Omega,REAL,u1,addreal) is ext-real V38() V39() Element of REAL
Sigma --> 1 is Relation-like Sigma -defined NAT -valued RAT -valued INT -valued Function-like non empty finite total quasi_total V146() V147() V148() V149() Element of bool [:Sigma,NAT:]
[:Sigma,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Sigma,NAT:] is non empty non trivial non finite set
dom (Sigma --> 1) is non empty finite Element of bool Sigma
rng (Sigma --> 1) is non empty finite V139() V140() V141() V142() V143() V144() Element of bool REAL
G2 is set
(Sigma --> 1) . G2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
P2M v1 is Relation-like Trivial-SigmaField Sigma -defined ExtREAL -valued Function-like non empty finite total quasi_total V147() V155() nonnegative V204(Sigma, Trivial-SigmaField Sigma) Element of bool [:(Trivial-SigmaField Sigma),ExtREAL:]
[:(Trivial-SigmaField Sigma),ExtREAL:] is Relation-like non empty V147() set
bool [:(Trivial-SigmaField Sigma),ExtREAL:] is non empty set
f2 is Relation-like Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Sigma,REAL:]
Integral ((P2M v1),f2) is ext-real Element of ExtREAL
(P2M v1) . Sigma is ext-real Element of ExtREAL
(R_EAL 1) * ((P2M v1) . Sigma) is ext-real Element of ExtREAL
v1 . Sigma is ext-real V38() V39() Element of REAL
1 * (v1 . Sigma) is ext-real V38() V39() Element of REAL
card Sigma 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
G2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
len G2 is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
s2 is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
rng s2 is finite Element of bool Sigma
len s2 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 G2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Sum G2 is ext-real V38() V39() Element of REAL
addreal "**" G2 is ext-real V38() V39() Element of REAL
dom h is non empty finite Element of bool Sigma
Y2 is finite Element of bool Sigma
h * s2 is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() Element of bool [:NAT,REAL:]
dom (h * s2) is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
dom s2 is finite V139() V140() V141() V142() V143() V144() Element of bool NAT
Seg (len s2) is finite len s2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ 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 <= b₁ & b₁ <= len s2 ) } is set
Y3 is set
G2 . Y3 is ext-real V38() V39() Element of REAL
x is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
s2 . x is set
f2 . (s2 . x) is ext-real V38() V39() Element of REAL
{(s2 . x)} is non empty trivial finite 1 -element set
v1 . {(s2 . x)} is ext-real V38() V39() Element of REAL
(f2 . (s2 . x)) * (v1 . {(s2 . x)}) is ext-real V38() V39() Element of REAL
1 * (v1 . {(s2 . x)}) is ext-real V38() V39() Element of REAL
h . (s2 . x) is ext-real V38() V39() Element of REAL
(h * s2) . Y3 is ext-real V38() V39() Element of REAL
Func_Seq (h,s2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V146() V147() V148() FinSequence of REAL
s2 (#) h is Relation-like NAT -defined REAL -valued Function-like finite V146() V147() V148() set
[:Y1,Y2:] is Relation-like finite set
x is set
y is set
g . (x,y) is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V31() set
g . [x,y] is ext-real V38() V39() set
v . {x} is ext-real V38() V39() Element of REAL
{y} is non empty trivial finite 1 -element set
v1 . {y} is ext-real V38() V39() Element of REAL
(v . {x}) * (v1 . {y}) is ext-real V38() V39() Element of REAL
u1 . x is ext-real V38() V39() Element of REAL
(u1 . x) * (v1 . {y}) is ext-real V38() V39() Element of REAL
h . y is ext-real V38() V39() Element of REAL
(u1 . x) * (h . y) is ext-real V38() V39() Element of REAL
Y3 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (Y3,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
setopfunc (Y2,Sigma,REAL,h,addreal) is ext-real V38() V39() Element of REAL
(setopfunc (Y1,Omega,REAL,u1,addreal)) * (setopfunc (Y2,Sigma,REAL,h,addreal)) 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
bool [:Omega,Sigma:] is non empty finite V31() set
[:(bool [:Omega,Sigma:]),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(bool [:Omega,Sigma:]),REAL:] is non empty non trivial non finite set
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
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 bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
h is set
y is set
y is set
[y,y] is set
{y,y} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,y},{y}} is non empty finite V31() set
s1 is set
{y} is non empty trivial finite 1 -element set
s1 is set
g . h is ext-real V38() V39() Element of REAL
g . (y,y) is set
g . [y,y] is ext-real V38() V39() set
v . {y} is ext-real V38() V39() Element of REAL
v1 . {y} is ext-real V38() V39() Element of REAL
(v . {y}) * (v1 . {y}) is ext-real V38() V39() Element of REAL
h is set
u . h is ext-real V38() V39() Element of REAL
y is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
y is set
g . y is ext-real V38() V39() Element of REAL
setopfunc (y,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
u1 is Relation-like Omega -defined Sigma -valued finite Element of bool [:Omega,Sigma:]
setopfunc (u1,[:Omega,Sigma:],REAL,g,addreal) is ext-real V38() V39() Element of REAL
u . [:Omega,Sigma:] 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
Trivial-SigmaField [:Omega,Sigma:] is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203([:Omega,Sigma:]) Element of bool (bool [:Omega,Sigma:])
bool [:Omega,Sigma:] is non empty finite V31() set
bool (bool [:Omega,Sigma:]) is non empty finite V31() 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
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
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:]
[:(bool [:Omega,Sigma:]),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(bool [:Omega,Sigma:]),REAL:] is non empty non trivial non finite set
u is Relation-like bool [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool [:Omega,Sigma:]),REAL:]
u1 is set
u . u1 is ext-real V38() V39() Element of REAL
u . [:Omega,Sigma:] is ext-real V38() V39() Element of REAL
g is Relation-like Trivial-SigmaField [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField [:Omega,Sigma:]
u is Relation-like Trivial-SigmaField [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField [:Omega,Sigma:]
u1 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 Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
h 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:]
h 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:]
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
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
(Omega,Sigma,v,v1) is Relation-like Trivial-SigmaField [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField [:Omega,Sigma:]
[:Omega,Sigma:] is Relation-like non empty finite set
Trivial-SigmaField [:Omega,Sigma:] is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203([:Omega,Sigma:]) Element of bool (bool [:Omega,Sigma:])
bool [:Omega,Sigma:] is non empty finite V31() set
bool (bool [:Omega,Sigma:]) is non empty finite V31() set
g is non empty finite Element of bool Omega
v . g is ext-real V38() V39() Element of REAL
u is non empty finite Element of bool Sigma
[:g,u:] is Relation-like non empty finite set
(Omega,Sigma,v,v1) . [:g,u:] is ext-real V38() V39() Element of REAL
v1 . u is ext-real V38() V39() Element of REAL
(v . g) * (v1 . u) is ext-real V38() V39() Element of REAL
[:[: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
h 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:]
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
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
(Omega,Sigma,v,v1) is Relation-like Trivial-SigmaField [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField [:Omega,Sigma:]
[:Omega,Sigma:] is Relation-like non empty finite set
Trivial-SigmaField [:Omega,Sigma:] is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203([:Omega,Sigma:]) Element of bool (bool [:Omega,Sigma:])
bool [:Omega,Sigma:] is non empty finite V31() set
bool (bool [:Omega,Sigma:]) is non empty finite V31() set
g is set
u is set
[g,u] is set
{g,u} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,u},{g}} is non empty finite V31() set
{[g,u]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(Omega,Sigma,v,v1) . {[g,u]} is ext-real V38() V39() Element of REAL
v . {g} is ext-real V38() V39() Element of REAL
{u} is non empty trivial finite 1 -element set
v1 . {u} is ext-real V38() V39() Element of REAL
(v . {g}) * (v1 . {u}) is ext-real V38() V39() Element of REAL
u1 is set
[:{g},{u}:] is Relation-like non empty finite 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)
{ b₁ where b₁ is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma : verum } is set
RAlgebra Omega is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V105() V107() V109() V111() V113() strict vector-associative AlgebraStr
Funcs (Omega,REAL) is functional non empty FUNCTION_DOMAIN of Omega, REAL
RealFuncMult Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] is Relation-like non empty set
[:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty set
RealFuncAdd Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
RealFuncExtMult Omega is Relation-like [:REAL,(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:REAL,(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty non trivial non finite set
RealFuncUnit Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
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
RealFuncZero Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega --> 0 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:]
AlgebraStr(# (Funcs (Omega,REAL)),(RealFuncMult Omega),(RealFuncAdd Omega),(RealFuncExtMult Omega),(RealFuncUnit Omega),(RealFuncZero Omega) #) is strict AlgebraStr
the U1 of (RAlgebra Omega) is set
bool the U1 of (RAlgebra Omega) is non empty set
the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v is set
v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
RAlgebra Omega is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V105() V107() V109() V111() V113() strict vector-associative AlgebraStr
Funcs (Omega,REAL) is functional non empty FUNCTION_DOMAIN of Omega, REAL
RealFuncMult Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] is Relation-like non empty set
[:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty set
RealFuncAdd Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
RealFuncExtMult Omega is Relation-like [:REAL,(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:REAL,(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty non trivial non finite set
RealFuncUnit Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
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
RealFuncZero Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega --> 0 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:]
AlgebraStr(# (Funcs (Omega,REAL)),(RealFuncMult Omega),(RealFuncAdd Omega),(RealFuncExtMult Omega),(RealFuncUnit Omega),(RealFuncZero Omega) #) is strict AlgebraStr
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
(Omega,Sigma) is non empty Element of bool the U1 of (RAlgebra Omega)
the U1 of (RAlgebra Omega) is set
bool the U1 of (RAlgebra Omega) is non empty set
{ b₁ where b₁ is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma : verum } is set
g is Element of the U1 of (RAlgebra Omega)
u is Element of the U1 of (RAlgebra Omega)
g * u is Element of the U1 of (RAlgebra Omega)
the U6 of (RAlgebra Omega) is Relation-like [: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):] -defined the U1 of (RAlgebra Omega) -valued Function-like quasi_total Element of bool [:[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):]
[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):] is Relation-like set
[:[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is Relation-like set
bool [:[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is non empty set
the U6 of (RAlgebra Omega) . (g,u) is Element of the U1 of (RAlgebra Omega)
[g,u] is set
{g,u} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,u},{g}} is non empty finite V31() set
the U6 of (RAlgebra Omega) . [g,u] is set
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
dom y is non empty Element of bool Omega
dom u1 is non empty Element of bool Omega
(dom y) /\ (dom u1) is Element of bool Omega
Omega /\ (dom u1) is Element of bool Omega
h is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega /\ Omega is set
dom h is Element of bool Omega
y is set
h . y is ext-real V38() V39() Element of REAL
y . y is ext-real V38() V39() Element of REAL
u1 . y is ext-real V38() V39() Element of REAL
(y . y) * (u1 . y) is ext-real V38() V39() Element of REAL
y (#) u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
y is Relation-like Function-like set
dom y is set
rng y is set
g is Element of the U1 of (RAlgebra Omega)
u is Element of the U1 of (RAlgebra Omega)
g + u is Element of the U1 of (RAlgebra Omega)
the U5 of (RAlgebra Omega) is Relation-like [: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):] -defined the U1 of (RAlgebra Omega) -valued Function-like quasi_total Element of bool [:[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):]
[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):] is Relation-like set
[:[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is Relation-like set
bool [:[: the U1 of (RAlgebra Omega), the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is non empty set
the U5 of (RAlgebra Omega) . (g,u) is Element of the U1 of (RAlgebra Omega)
[g,u] is set
{g,u} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,u},{g}} is non empty finite V31() set
the U5 of (RAlgebra Omega) . [g,u] is set
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
dom y is non empty Element of bool Omega
dom u1 is non empty Element of bool Omega
(dom y) /\ (dom u1) is Element of bool Omega
Omega /\ (dom u1) is Element of bool Omega
h is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega /\ Omega is set
dom h is Element of bool Omega
y is set
h . y is ext-real V38() V39() Element of REAL
y . y is ext-real V38() V39() Element of REAL
u1 . y is ext-real V38() V39() Element of REAL
(y . y) + (u1 . y) is ext-real V38() V39() Element of REAL
y + u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
y is Relation-like Function-like set
dom y is set
rng y is set
g is Element of the U1 of (RAlgebra Omega)
- g is Element of the U1 of (RAlgebra Omega)
u is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- 1 is non empty ext-real non positive negative V38() V39() V104() V161() Element of INT
- u is Relation-like Omega -defined REAL -valued Function-like 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
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) u is Relation-like Function-like set
u1 is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
(- 1) * g is Element of the U1 of (RAlgebra Omega)
the Mult of (RAlgebra Omega) is Relation-like [:REAL, the U1 of (RAlgebra Omega):] -defined the U1 of (RAlgebra Omega) -valued Function-like quasi_total Element of bool [:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):]
[:REAL, the U1 of (RAlgebra Omega):] is Relation-like set
[:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is Relation-like set
bool [:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is non empty set
the Mult of (RAlgebra Omega) . ((- 1),g) is set
[(- 1),g] is set
{(- 1),g} is non empty finite set
{(- 1)} is non empty trivial finite 1 -element V139() V140() V141() V142() V143() set
{{(- 1),g},{(- 1)}} is non empty finite V31() set
the Mult of (RAlgebra Omega) . [(- 1),g] is set
h is set
dom u1 is Element of bool Omega
u1 . h is ext-real V38() V39() Element of REAL
y is Element of Omega
u . y is ext-real V38() V39() Element of REAL
(- 1) * (u . y) is ext-real V38() V39() Element of REAL
u . h is ext-real V38() V39() Element of REAL
- (u . h) is ext-real V38() V39() Element of REAL
dom u is non empty Element of bool Omega
h is Relation-like Function-like set
dom h is set
rng h is set
g is ext-real V38() V39() Element of REAL
u is Element of the U1 of (RAlgebra Omega)
g * u is Element of the U1 of (RAlgebra Omega)
the Mult of (RAlgebra Omega) is Relation-like [:REAL, the U1 of (RAlgebra Omega):] -defined the U1 of (RAlgebra Omega) -valued Function-like quasi_total Element of bool [:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):]
[:REAL, the U1 of (RAlgebra Omega):] is Relation-like set
[:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is Relation-like set
bool [:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is non empty set
the Mult of (RAlgebra Omega) . (g,u) is set
[g,u] is set
{g,u} is non empty finite set
{g} is non empty trivial finite 1 -element V139() V140() V141() set
{{g,u},{g}} is non empty finite V31() set
the Mult of (RAlgebra Omega) . [g,u] is set
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
h is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
dom u1 is non empty Element of bool Omega
dom h is Element of bool Omega
y is set
h . y is ext-real V38() V39() Element of REAL
u1 . y is ext-real V38() V39() Element of REAL
g * (u1 . y) is ext-real V38() V39() Element of REAL
g (#) u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
y is Relation-like Function-like set
dom y is set
rng y is 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
g is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
1. (RAlgebra Omega) is Element of the U1 of (RAlgebra Omega)
the U3 of (RAlgebra Omega) is Element of the U1 of (RAlgebra Omega)
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
RAlgebra Omega is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V105() V107() V109() V111() V113() strict vector-associative AlgebraStr
Funcs (Omega,REAL) is functional non empty FUNCTION_DOMAIN of Omega, REAL
RealFuncMult Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] is Relation-like non empty set
[:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty set
RealFuncAdd Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
RealFuncExtMult Omega is Relation-like [:REAL,(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:REAL,(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty non trivial non finite set
RealFuncUnit Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
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
RealFuncZero Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega --> 0 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:]
AlgebraStr(# (Funcs (Omega,REAL)),(RealFuncMult Omega),(RealFuncAdd Omega),(RealFuncExtMult Omega),(RealFuncUnit Omega),(RealFuncZero Omega) #) is strict AlgebraStr
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
(Omega,Sigma) is non empty Element of bool the U1 of (RAlgebra Omega)
the U1 of (RAlgebra Omega) is set
bool the U1 of (RAlgebra Omega) is non empty set
{ b₁ where b₁ is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma : verum } 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)
(Omega,Sigma) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the U1 of (RAlgebra Omega)
RAlgebra Omega is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V105() V107() V109() V111() V113() strict vector-associative AlgebraStr
Funcs (Omega,REAL) is functional non empty FUNCTION_DOMAIN of Omega, REAL
RealFuncMult Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] is Relation-like non empty set
[:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty set
RealFuncAdd Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
RealFuncExtMult Omega is Relation-like [:REAL,(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:REAL,(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty non trivial non finite set
RealFuncUnit Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
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
RealFuncZero Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega --> 0 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:]
AlgebraStr(# (Funcs (Omega,REAL)),(RealFuncMult Omega),(RealFuncAdd Omega),(RealFuncExtMult Omega),(RealFuncUnit Omega),(RealFuncZero Omega) #) is strict AlgebraStr
the U1 of (RAlgebra Omega) is set
bool the U1 of (RAlgebra Omega) is non empty set
{ b₁ where b₁ is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma : verum } is set
mult_ ((Omega,Sigma),(RAlgebra Omega)) is Relation-like [:(Omega,Sigma),(Omega,Sigma):] -defined (Omega,Sigma) -valued Function-like non empty total quasi_total Element of bool [:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):]
[:(Omega,Sigma),(Omega,Sigma):] is Relation-like non empty set
[:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):] is Relation-like non empty set
bool [:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):] is non empty set
Add_ ((Omega,Sigma),(RAlgebra Omega)) is Relation-like [:(Omega,Sigma),(Omega,Sigma):] -defined (Omega,Sigma) -valued Function-like non empty total quasi_total Element of bool [:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):]
Mult_ ((Omega,Sigma),(RAlgebra Omega)) is Relation-like [:REAL,(Omega,Sigma):] -defined (Omega,Sigma) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Omega,Sigma):],(Omega,Sigma):]
[:REAL,(Omega,Sigma):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Omega,Sigma):],(Omega,Sigma):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Omega,Sigma):],(Omega,Sigma):] is non empty non trivial non finite set
One_ ((Omega,Sigma),(RAlgebra Omega)) is Element of (Omega,Sigma)
Zero_ ((Omega,Sigma),(RAlgebra Omega)) is Element of (Omega,Sigma)
AlgebraStr(# (Omega,Sigma),(mult_ ((Omega,Sigma),(RAlgebra Omega))),(Add_ ((Omega,Sigma),(RAlgebra Omega))),(Mult_ ((Omega,Sigma),(RAlgebra Omega))),(One_ ((Omega,Sigma),(RAlgebra Omega))),(Zero_ ((Omega,Sigma),(RAlgebra Omega))) #) is strict AlgebraStr
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)
(Omega,Sigma) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V107() V109() V111() V113() vector-associative AlgebraStr
(Omega,Sigma) is non empty add-closed having-inverse additively-closed multiplicatively-closed additively-linearly-closed Element of bool the U1 of (RAlgebra Omega)
RAlgebra Omega is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V105() V107() V109() V111() V113() strict vector-associative AlgebraStr
Funcs (Omega,REAL) is functional non empty FUNCTION_DOMAIN of Omega, REAL
RealFuncMult Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] is Relation-like non empty set
[:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty set
RealFuncAdd Omega is Relation-like [:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs (Omega,REAL)),(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
RealFuncExtMult Omega is Relation-like [:REAL,(Funcs (Omega,REAL)):] -defined Funcs (Omega,REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):]
[:REAL,(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Funcs (Omega,REAL)):],(Funcs (Omega,REAL)):] is non empty non trivial non finite set
RealFuncUnit Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
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
RealFuncZero Omega is Relation-like Omega -defined REAL -valued Function-like total quasi_total V146() V147() V148() Element of Funcs (Omega,REAL)
Omega --> 0 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:]
AlgebraStr(# (Funcs (Omega,REAL)),(RealFuncMult Omega),(RealFuncAdd Omega),(RealFuncExtMult Omega),(RealFuncUnit Omega),(RealFuncZero Omega) #) is strict AlgebraStr
the U1 of (RAlgebra Omega) is set
bool the U1 of (RAlgebra Omega) is non empty set
{ b₁ where b₁ is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma : verum } is set
mult_ ((Omega,Sigma),(RAlgebra Omega)) is Relation-like [:(Omega,Sigma),(Omega,Sigma):] -defined (Omega,Sigma) -valued Function-like non empty total quasi_total Element of bool [:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):]
[:(Omega,Sigma),(Omega,Sigma):] is Relation-like non empty set
[:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):] is Relation-like non empty set
bool [:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):] is non empty set
Add_ ((Omega,Sigma),(RAlgebra Omega)) is Relation-like [:(Omega,Sigma),(Omega,Sigma):] -defined (Omega,Sigma) -valued Function-like non empty total quasi_total Element of bool [:[:(Omega,Sigma),(Omega,Sigma):],(Omega,Sigma):]
Mult_ ((Omega,Sigma),(RAlgebra Omega)) is Relation-like [:REAL,(Omega,Sigma):] -defined (Omega,Sigma) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Omega,Sigma):],(Omega,Sigma):]
[:REAL,(Omega,Sigma):] is Relation-like non empty non trivial non finite set
[:[:REAL,(Omega,Sigma):],(Omega,Sigma):] is Relation-like non empty non trivial non finite set
bool [:[:REAL,(Omega,Sigma):],(Omega,Sigma):] is non empty non trivial non finite set
One_ ((Omega,Sigma),(RAlgebra Omega)) is Element of (Omega,Sigma)
Zero_ ((Omega,Sigma),(RAlgebra Omega)) is Element of (Omega,Sigma)
AlgebraStr(# (Omega,Sigma),(mult_ ((Omega,Sigma),(RAlgebra Omega))),(Add_ ((Omega,Sigma),(RAlgebra Omega))),(Mult_ ((Omega,Sigma),(RAlgebra Omega))),(One_ ((Omega,Sigma),(RAlgebra Omega))),(Zero_ ((Omega,Sigma),(RAlgebra Omega))) #) is strict AlgebraStr
the U1 of (Omega,Sigma) is set
v is Element of the U1 of (Omega,Sigma)
1 * v is Element of the U1 of (Omega,Sigma)
the Mult of (Omega,Sigma) is Relation-like [:REAL, the U1 of (Omega,Sigma):] -defined the U1 of (Omega,Sigma) -valued Function-like quasi_total Element of bool [:[:REAL, the U1 of (Omega,Sigma):], the U1 of (Omega,Sigma):]
[:REAL, the U1 of (Omega,Sigma):] is Relation-like set
[:[:REAL, the U1 of (Omega,Sigma):], the U1 of (Omega,Sigma):] is Relation-like set
bool [:[:REAL, the U1 of (Omega,Sigma):], the U1 of (Omega,Sigma):] is non empty set
the Mult of (Omega,Sigma) . (1,v) is set
[1,v] is set
{1,v} is non empty finite set
{{1,v},{1}} is non empty finite V31() set
the Mult of (Omega,Sigma) . [1,v] is set
v1 is Element of the U1 of (RAlgebra Omega)
1 * v1 is Element of the U1 of (RAlgebra Omega)
the Mult of (RAlgebra Omega) is Relation-like [:REAL, the U1 of (RAlgebra Omega):] -defined the U1 of (RAlgebra Omega) -valued Function-like quasi_total Element of bool [:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):]
[:REAL, the U1 of (RAlgebra Omega):] is Relation-like set
[:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is Relation-like set
bool [:[:REAL, the U1 of (RAlgebra Omega):], the U1 of (RAlgebra Omega):] is non empty set
the Mult of (RAlgebra Omega) . (1,v1) is set
[1,v1] is set
{1,v1} is non empty finite set
{{1,v1},{1}} is non empty finite V31() set
the Mult of (RAlgebra Omega) . [1,v1] is set