:: CARDFIN2 semantic presentation

REAL is non empty V2() non finite V50() V51() V52() V56() set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal non finite V50() V51() V52() V53() V54() V55() V56() cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is V2() non finite set
COMPLEX is non empty V2() non finite V50() V56() set
RAT is non empty V2() non finite V50() V51() V52() V53() V56() set
INT is non empty V2() non finite V50() V51() V52() V53() V54() V56() set
K7(NAT,REAL) is V2() Relation-like V33() V34() V35() non finite set
K6(K7(NAT,REAL)) is V2() non finite set
omega is non empty V2() epsilon-transitive epsilon-connected ordinal non finite V50() V51() V52() V53() V54() V55() V56() cardinal limit_cardinal set
K6(omega) is V2() non finite set
K6(NAT) is V2() non finite set
K7(NAT,COMPLEX) is V2() Relation-like V33() non finite set
K6(K7(NAT,COMPLEX)) is V2() non finite set
K7(COMPLEX,COMPLEX) is V2() Relation-like V33() non finite set
K6(K7(COMPLEX,COMPLEX)) is V2() non finite set
K7(REAL,REAL) is V2() Relation-like V33() V34() V35() non finite set
K6(K7(REAL,REAL)) is V2() non finite set
K69(REAL,REAL) is set
K7(NAT,K69(REAL,REAL)) is Relation-like set
K6(K7(NAT,K69(REAL,REAL))) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
{{},1} is non empty finite V48() V50() V51() V52() V53() V54() V55() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V2() Relation-like V33() non finite set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V2() non finite set
K7(K7(REAL,REAL),REAL) is V2() Relation-like V33() V34() V35() non finite set
K6(K7(K7(REAL,REAL),REAL)) is V2() non finite set
K7(RAT,RAT) is V2() Relation-like RAT -valued V33() V34() V35() non finite set
K6(K7(RAT,RAT)) is V2() non finite set
K7(K7(RAT,RAT),RAT) is V2() Relation-like RAT -valued V33() V34() V35() non finite set
K6(K7(K7(RAT,RAT),RAT)) is V2() non finite set
K7(INT,INT) is V2() Relation-like RAT -valued INT -valued V33() V34() V35() non finite set
K6(K7(INT,INT)) is V2() non finite set
K7(K7(INT,INT),INT) is V2() Relation-like RAT -valued INT -valued V33() V34() V35() non finite set
K6(K7(K7(INT,INT),INT)) is V2() non finite set
K7(NAT,NAT) is V2() Relation-like RAT -valued INT -valued V33() V34() V35() V36() non finite set
K7(K7(NAT,NAT),NAT) is V2() Relation-like RAT -valued INT -valued V33() V34() V35() V36() non finite set
K6(K7(K7(NAT,NAT),NAT)) is V2() non finite set
K588() is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
- 1 is non empty complex real ext-real non positive negative integer V49() Element of INT
1 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
Prod_real_n . 1 is complex real ext-real Element of REAL
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V49() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() Element of NAT
number_e is complex real ext-real Element of REAL
exp_R is non empty Relation-like REAL -defined REAL -valued Function-like V23( REAL ) quasi_total V33() V34() V35() continuous Element of K6(K7(REAL,REAL))
dom exp_R is non empty V50() V51() V52() Element of K6(REAL)
K323(exp_R,0) is complex real ext-real Element of REAL
addint is Relation-like K7(INT,INT) -defined RAT -valued INT -valued Function-like V23(K7(INT,INT)) quasi_total V33() V34() V35() V92( INT ) V110( INT ) V111( INT ) Element of K6(K7(K7(INT,INT),INT))
number_e is complex real ext-real set
exp_R 1 is complex real ext-real Element of REAL
K323(exp_R,1) is complex real ext-real Element of REAL
- 1 is non empty complex real ext-real non positive negative integer set
Funcs ({},{}) is non empty functional finite set
id {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding {} -defined {} -valued RAT -valued INT -valued Function-like one-to-one constant functional V23( {} ) ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
{(id {})} is non empty V2() functional finite V48() V50() V51() V52() V53() V54() V55() 1 -element set
j is complex real ext-real set
exp_R j is complex real ext-real set
K323(exp_R,j) is complex real ext-real Element of REAL
id {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding {} -defined {} -valued RAT -valued INT -valued Function-like one-to-one constant functional V23( {} ) quasi_total ext-real non positive non negative V33() V34() V35() V36() V37() V39() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() Element of K6(K7({},{}))
K7({},{}) is Relation-like RAT -valued INT -valued V33() V34() V35() V36() finite set
K6(K7({},{})) is finite V48() set
j is set
dom (id {}) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() Element of K6(NAT)
j is complex real ext-real set
exp_R j is non empty complex real ext-real positive non negative set
K323(exp_R,j) is complex real ext-real Element of REAL
j is complex real ext-real set
1 / 2 is non empty complex real ext-real positive non negative V49() Element of RAT
2 " is non empty complex real ext-real positive non negative set
1 * (2 ") is non empty complex real ext-real positive non negative set
j + (1 / 2) is complex real ext-real Element of REAL
[\(j + (1 / 2))/] is complex real ext-real integer set
j is complex real ext-real integer set
(j) is complex real ext-real integer set
j + (1 / 2) is complex real ext-real Element of REAL
[\(j + (1 / 2))/] is complex real ext-real integer set
j - 0 is complex real ext-real integer V49() Element of INT
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
j + (- 0) is complex real ext-real integer set
j - (1 / 2) is complex real ext-real Element of REAL
- (1 / 2) is non empty complex real ext-real non positive negative set
j + (- (1 / 2)) is complex real ext-real set
j + 0 is complex real ext-real integer V49() Element of INT
(j + (1 / 2)) - 1 is complex real ext-real Element of REAL
(j + (1 / 2)) + (- 1) is complex real ext-real set
j is complex real ext-real integer set
z is complex real ext-real set
j - z is complex real ext-real Element of REAL
- z is complex real ext-real set
j + (- z) is complex real ext-real set
|.(j - z).| is complex real ext-real Element of REAL
(z) is complex real ext-real integer set
z + (1 / 2) is complex real ext-real Element of REAL
[\(z + (1 / 2))/] is complex real ext-real integer set
(1 / 2) + z is complex real ext-real Element of REAL
(j - z) + z is complex real ext-real Element of REAL
- (1 / 2) is non empty complex real ext-real non positive negative V49() Element of RAT
- (- (1 / 2)) is non empty complex real ext-real positive non negative V49() Element of RAT
- (j - z) is complex real ext-real Element of REAL
(1 / 2) + j is complex real ext-real Element of REAL
z - j is complex real ext-real Element of REAL
- j is complex real ext-real integer set
z + (- j) is complex real ext-real set
(z - j) + j is complex real ext-real Element of REAL
j + (1 / 2) is complex real ext-real Element of REAL
(j + (1 / 2)) - (1 / 2) is complex real ext-real Element of REAL
- (1 / 2) is non empty complex real ext-real non positive negative set
(j + (1 / 2)) + (- (1 / 2)) is complex real ext-real set
z - (1 / 2) is complex real ext-real Element of REAL
z + (- (1 / 2)) is complex real ext-real set
(z + (1 / 2)) - 1 is complex real ext-real Element of REAL
(z + (1 / 2)) + (- 1) is complex real ext-real set
[#] REAL is V50() V51() V52() V84() V85() Element of K6(REAL)
j is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(j + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (j + 1) is complex real ext-real Element of REAL
s is complex real ext-real set
z is complex real ext-real set
].z,s.[ is V50() V51() V52() V85() Element of K6(REAL)
exp_R z is non empty complex real ext-real positive non negative set
K323(exp_R,z) is complex real ext-real Element of REAL
Taylor (exp_R,([#] REAL),s,z) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (Taylor (exp_R,([#] REAL),s,z)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (Taylor (exp_R,([#] REAL),s,z))) . j is complex real ext-real Element of REAL
z - s is complex real ext-real Element of REAL
- s is complex real ext-real set
z + (- s) is complex real ext-real set
(z - s) |^ (j + 1) is complex real ext-real Element of REAL
diff (exp_R,([#] REAL)) is Relation-like NAT -defined K69(REAL,REAL) -valued Function-like quasi_total Element of K6(K7(NAT,K69(REAL,REAL)))
(diff (exp_R,([#] REAL))) . j is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
exp_R | ([#] REAL) is Relation-like REAL -defined [#] REAL -defined REAL -defined REAL -valued Function-like V33() V34() V35() continuous Element of K6(K7(REAL,REAL))
[.z,s.] is V50() V51() V52() V84() Element of K6(REAL)
((diff (exp_R,([#] REAL))) . j) | [.z,s.] is Relation-like REAL -defined [.z,s.] -defined REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
exp_R . z is complex real ext-real set
diff (exp_R,].z,s.[) is Relation-like NAT -defined K69(REAL,REAL) -valued Function-like quasi_total Element of K6(K7(NAT,K69(REAL,REAL)))
(diff (exp_R,].z,s.[)) . (j + 1) is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
comega is complex real ext-real Element of REAL
((diff (exp_R,].z,s.[)) . (j + 1)) . comega is complex real ext-real set
(((diff (exp_R,].z,s.[)) . (j + 1)) . comega) * ((z - s) |^ (j + 1)) is complex real ext-real Element of REAL
((((diff (exp_R,].z,s.[)) . (j + 1)) . comega) * ((z - s) |^ (j + 1))) / ((j + 1) !) is complex real ext-real Element of REAL
((j + 1) !) " is non empty complex real ext-real positive non negative set
((((diff (exp_R,].z,s.[)) . (j + 1)) . comega) * ((z - s) |^ (j + 1))) * (((j + 1) !) ") is complex real ext-real set
((Partial_Sums (Taylor (exp_R,([#] REAL),s,z))) . j) + (((((diff (exp_R,].z,s.[)) . (j + 1)) . comega) * ((z - s) |^ (j + 1))) / ((j + 1) !)) is complex real ext-real Element of REAL
exp_R comega is non empty complex real ext-real positive non negative set
K323(exp_R,comega) is complex real ext-real Element of REAL
(exp_R comega) * ((z - s) |^ (j + 1)) is complex real ext-real Element of REAL
((exp_R comega) * ((z - s) |^ (j + 1))) / ((j + 1) !) is complex real ext-real Element of REAL
((exp_R comega) * ((z - s) |^ (j + 1))) * (((j + 1) !) ") is complex real ext-real set
((Partial_Sums (Taylor (exp_R,([#] REAL),s,z))) . j) + (((exp_R comega) * ((z - s) |^ (j + 1))) / ((j + 1) !)) is complex real ext-real Element of REAL
j is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
j ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . j is complex real ext-real Element of REAL
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(- 1) |^ (j + 1) is complex real ext-real set
(j + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (j + 1) is complex real ext-real Element of REAL
z is complex real ext-real set
exp_R z is non empty complex real ext-real positive non negative set
K323(exp_R,z) is complex real ext-real Element of REAL
(exp_R z) * ((- 1) |^ (j + 1)) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) |^ (j + 1))) / ((j + 1) !) is complex real ext-real Element of REAL
((j + 1) !) " is non empty complex real ext-real positive non negative set
((exp_R z) * ((- 1) |^ (j + 1))) * (((j + 1) !) ") is complex real ext-real set
(j !) * (((exp_R z) * ((- 1) |^ (j + 1))) / ((j + 1) !)) is complex real ext-real Element of REAL
- ((j !) * (((exp_R z) * ((- 1) |^ (j + 1))) / ((j + 1) !))) is complex real ext-real Element of REAL
|.(- ((j !) * (((exp_R z) * ((- 1) |^ (j + 1))) / ((j + 1) !)))).| is complex real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(exp_R z) / (j + 1) is non empty complex real ext-real positive non negative Element of REAL
(j + 1) " is non empty complex real ext-real positive non negative set
(exp_R z) * ((j + 1) ") is non empty complex real ext-real positive non negative set
(exp_R z) / 2 is non empty complex real ext-real positive non negative Element of REAL
(exp_R z) * (2 ") is non empty complex real ext-real positive non negative set
(- 1) |^ j is complex real ext-real set
(exp_R z) * ((- 1) |^ j) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) |^ j)) / (j + 1) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) |^ j)) * ((j + 1) ") is complex real ext-real set
|.(((exp_R z) * ((- 1) |^ j)) / (j + 1)).| is complex real ext-real Element of REAL
(- 1) to_power j is complex real ext-real set
1 to_power j is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
1 |^ j is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
- (1 / 2) is non empty complex real ext-real non positive negative V49() Element of RAT
(- 1) to_power j is complex real ext-real set
- ((exp_R z) / (j + 1)) is non empty complex real ext-real non positive negative Element of REAL
- (1 / 2) is non empty complex real ext-real non positive negative V49() Element of RAT
((- 1) |^ j) * (- 1) is complex real ext-real Element of REAL
(- 1) * (((- 1) |^ j) * (- 1)) is complex real ext-real Element of REAL
(exp_R z) * ((- 1) * (((- 1) |^ j) * (- 1))) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) * (((- 1) |^ j) * (- 1)))) / (j + 1) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) * (((- 1) |^ j) * (- 1)))) * ((j + 1) ") is complex real ext-real set
(- 1) * ((- 1) |^ (j + 1)) is complex real ext-real Element of REAL
(exp_R z) * ((- 1) * ((- 1) |^ (j + 1))) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) * ((- 1) |^ (j + 1)))) / (j + 1) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) * ((- 1) |^ (j + 1)))) * ((j + 1) ") is complex real ext-real set
1 / (j + 1) is non empty complex real ext-real positive non negative V49() Element of RAT
1 * ((j + 1) ") is non empty complex real ext-real positive non negative set
((exp_R z) * ((- 1) |^ (j + 1))) * (1 / (j + 1)) is complex real ext-real Element of REAL
- (((exp_R z) * ((- 1) |^ (j + 1))) * (1 / (j + 1))) is complex real ext-real Element of REAL
(j !) / (j !) is non empty complex real ext-real positive non negative Element of REAL
(j !) " is non empty complex real ext-real positive non negative set
(j !) * ((j !) ") is non empty complex real ext-real positive non negative set
((j !) / (j !)) / (j + 1) is non empty complex real ext-real positive non negative Element of REAL
((j !) / (j !)) * ((j + 1) ") is non empty complex real ext-real positive non negative set
((exp_R z) * ((- 1) |^ (j + 1))) * (((j !) / (j !)) / (j + 1)) is complex real ext-real Element of REAL
- (((exp_R z) * ((- 1) |^ (j + 1))) * (((j !) / (j !)) / (j + 1))) is complex real ext-real Element of REAL
(j !) * (j + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(j !) / ((j !) * (j + 1)) is non empty complex real ext-real positive non negative Element of REAL
((j !) * (j + 1)) " is non empty complex real ext-real positive non negative set
(j !) * (((j !) * (j + 1)) ") is non empty complex real ext-real positive non negative set
((exp_R z) * ((- 1) |^ (j + 1))) * ((j !) / ((j !) * (j + 1))) is complex real ext-real Element of REAL
- (((exp_R z) * ((- 1) |^ (j + 1))) * ((j !) / ((j !) * (j + 1)))) is complex real ext-real Element of REAL
((exp_R z) * ((- 1) |^ (j + 1))) * (j !) is complex real ext-real Element of REAL
(j + 1) * (j !) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((exp_R z) * ((- 1) |^ (j + 1))) * (j !)) / ((j + 1) * (j !)) is complex real ext-real Element of REAL
((j + 1) * (j !)) " is non empty complex real ext-real positive non negative set
(((exp_R z) * ((- 1) |^ (j + 1))) * (j !)) * (((j + 1) * (j !)) ") is complex real ext-real set
- ((((exp_R z) * ((- 1) |^ (j + 1))) * (j !)) / ((j + 1) * (j !))) is complex real ext-real Element of REAL
(j !) * (exp_R z) is non empty complex real ext-real positive non negative Element of REAL
((j !) * (exp_R z)) * ((- 1) |^ (j + 1)) is complex real ext-real Element of REAL
(((j !) * (exp_R z)) * ((- 1) |^ (j + 1))) / ((j + 1) !) is complex real ext-real Element of REAL
(((j !) * (exp_R z)) * ((- 1) |^ (j + 1))) * (((j + 1) !) ") is complex real ext-real set
- ((((j !) * (exp_R z)) * ((- 1) |^ (j + 1))) / ((j + 1) !)) is complex real ext-real Element of REAL
j is set
K7(j,j) is Relation-like set
K6(K7(j,j)) is set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective Element of K6(K7(j,j)) : not b₁ is with_fixpoint } is set
j is finite set
(j) is set
K7(j,j) is Relation-like finite set
K6(K7(j,j)) is finite V48() set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective Element of K6(K7(j,j)) : not b₁ is with_fixpoint } is set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective finite Element of K6(K7(j,j)) } is set
card { b₁ where b₁ is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective finite Element of K6(K7(j,j)) } is epsilon-transitive epsilon-connected ordinal cardinal set
card j is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(card j) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (card j) is complex real ext-real Element of REAL
z is set
s is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective finite Element of K6(K7(j,j))
card (j) is epsilon-transitive epsilon-connected ordinal cardinal set
j is finite set
(j) is finite set
K7(j,j) is Relation-like finite set
K6(K7(j,j)) is finite V48() set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective Element of K6(K7(j,j)) : not b₁ is with_fixpoint } is set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in j or not b₁ . b₂ = b₂ ) ) ) } is set
s is set
t is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective finite Element of K6(K7(j,j))
E is set
t . E is set
s is set
t is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j))
card j is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
E is set
dom t is finite Element of K6(j)
K6(j) is finite V48() set
t . E is set
].(- 1),0.[ is V50() V51() V52() V85() Element of K6(REAL)
j is non empty finite set
(j) is finite set
K7(j,j) is Relation-like finite set
K6(K7(j,j)) is finite V48() set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective Element of K6(K7(j,j)) : not b₁ is with_fixpoint } is set
card (j) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
card j is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(card j) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (card j) is complex real ext-real Element of REAL
((card j) !) / number_e is non empty complex real ext-real positive non negative Element of REAL
number_e " is non empty complex real ext-real positive non negative set
((card j) !) * (number_e ") is non empty complex real ext-real positive non negative set
(card (j)) - (((card j) !) / number_e) is complex real ext-real Element of REAL
- (((card j) !) / number_e) is non empty complex real ext-real non positive negative set
(card (j)) + (- (((card j) !) / number_e)) is complex real ext-real set
(card j) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(- 1) |^ ((card j) + 1) is complex real ext-real set
((card j) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . ((card j) + 1) is complex real ext-real Element of REAL
{ b₁ where b₁ is non empty Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in j or not b₁ . b₂ = b₂ ) ) ) } is set
card { b₁ where b₁ is non empty Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in j or not b₁ . b₂ = b₂ ) ) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
s is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
Sum s is complex real ext-real integer Element of COMPLEX
dom s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
Taylor (exp_R,([#] REAL),0,(- 1)) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
exp_R (- 1) is non empty complex real ext-real positive non negative set
K323(exp_R,(- 1)) is complex real ext-real Element of REAL
Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card j) is complex real ext-real Element of REAL
(- 1) - 0 is non empty complex real ext-real non positive negative integer V49() Element of INT
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
(- 1) + (- 0) is non empty complex real ext-real non positive negative integer set
((- 1) - 0) |^ ((card j) + 1) is complex real ext-real set
E is complex real ext-real set
exp_R E is non empty complex real ext-real positive non negative set
K323(exp_R,E) is complex real ext-real Element of REAL
(exp_R E) * (((- 1) - 0) |^ ((card j) + 1)) is complex real ext-real Element of REAL
((exp_R E) * (((- 1) - 0) |^ ((card j) + 1))) / (((card j) + 1) !) is complex real ext-real Element of REAL
(((card j) + 1) !) " is non empty complex real ext-real positive non negative set
((exp_R E) * (((- 1) - 0) |^ ((card j) + 1))) * ((((card j) + 1) !) ") is complex real ext-real set
((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card j)) + (((exp_R E) * (((- 1) - 0) |^ ((card j) + 1))) / (((card j) + 1) !)) is complex real ext-real Element of REAL
((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
((card j) !) (#) (Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card j) is complex real ext-real Element of REAL
((card j) !) * ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card j)) is complex real ext-real Element of REAL
K7(NAT,INT) is V2() Relation-like RAT -valued INT -valued V33() V34() V35() non finite set
K6(K7(NAT,INT)) is V2() non finite set
s . 0 is complex real ext-real integer set
len s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
addint "**" s is complex real ext-real integer V49() Element of INT
(len s) - 1 is complex real ext-real integer V49() Element of INT
(len s) + (- 1) is complex real ext-real integer set
comega is non empty Relation-like NAT -defined INT -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,INT))
comega . 0 is complex real ext-real integer V49() Element of INT
comega . ((len s) - 1) is complex real ext-real integer set
(Partial_Sums (((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . 0 is complex real ext-real Element of REAL
(((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . 0 is complex real ext-real Element of REAL
(Taylor (exp_R,([#] REAL),0,(- 1))) . 0 is complex real ext-real Element of REAL
((card j) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . 0) is complex real ext-real Element of REAL
diff (exp_R,([#] REAL)) is Relation-like NAT -defined K69(REAL,REAL) -valued Function-like quasi_total Element of K6(K7(NAT,K69(REAL,REAL)))
(diff (exp_R,([#] REAL))) . 0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,([#] REAL))) . 0) . 0 is complex real ext-real set
((- 1) - 0) |^ 0 is complex real ext-real set
(((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0) is complex real ext-real Element of REAL
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 0 is complex real ext-real Element of REAL
((((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0)) / (0 !) is complex real ext-real Element of REAL
(0 !) " is non empty complex real ext-real positive non negative set
((((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0)) * ((0 !) ") is complex real ext-real set
((card j) !) * (((((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0)) / (0 !)) is complex real ext-real Element of REAL
(- 1) |^ 0 is complex real ext-real set
1 * ((- 1) |^ 0) is complex real ext-real Element of REAL
(1 * ((- 1) |^ 0)) / (0 !) is complex real ext-real Element of REAL
(1 * ((- 1) |^ 0)) * ((0 !) ") is complex real ext-real set
((card j) !) * ((1 * ((- 1) |^ 0)) / (0 !)) is complex real ext-real Element of REAL
((card j) !) * ((- 1) |^ 0) is complex real ext-real Element of REAL
(((card j) !) * ((- 1) |^ 0)) / (0 !) is complex real ext-real Element of REAL
(((card j) !) * ((- 1) |^ 0)) * ((0 !) ") is complex real ext-real set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(Partial_Sums (((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . f is complex real ext-real Element of REAL
comega . f is complex real ext-real integer V49() Element of INT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(Partial_Sums (((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (f + 1) is complex real ext-real Element of REAL
comega . (f + 1) is complex real ext-real integer V49() Element of INT
(((card j) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . (f + 1) is complex real ext-real Element of REAL
(Taylor (exp_R,([#] REAL),0,(- 1))) . (f + 1) is complex real ext-real Element of REAL
((card j) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . (f + 1)) is complex real ext-real Element of REAL
diff (exp_R,([#] REAL)) is Relation-like NAT -defined K69(REAL,REAL) -valued Function-like quasi_total Element of K6(K7(NAT,K69(REAL,REAL)))
(diff (exp_R,([#] REAL))) . (f + 1) is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,([#] REAL))) . (f + 1)) . 0 is complex real ext-real set
((- 1) - 0) |^ (f + 1) is complex real ext-real set
(((diff (exp_R,([#] REAL))) . (f + 1)) . 0) * (((- 1) - 0) |^ (f + 1)) is complex real ext-real Element of REAL
(f + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (f + 1) is complex real ext-real Element of REAL
((((diff (exp_R,([#] REAL))) . (f + 1)) . 0) * (((- 1) - 0) |^ (f + 1))) / ((f + 1) !) is complex real ext-real Element of REAL
((f + 1) !) " is non empty complex real ext-real positive non negative set
((((diff (exp_R,([#] REAL))) . (f + 1)) . 0) * (((- 1) - 0) |^ (f + 1))) * (((f + 1) !) ") is complex real ext-real set
((card j) !) * (((((diff (exp_R,([#] REAL))) . (f + 1)) . 0) * (((- 1) - 0) |^ (f + 1))) / ((f + 1) !)) is complex real ext-real Element of REAL
(- 1) |^ (f + 1) is complex real ext-real set
1 * ((- 1) |^ (f + 1)) is complex real ext-real Element of REAL
(1 * ((- 1) |^ (f + 1))) / ((f + 1) !) is complex real ext-real Element of REAL
(1 * ((- 1) |^ (f + 1))) * (((f + 1) !) ") is complex real ext-real set
((card j) !) * ((1 * ((- 1) |^ (f + 1))) / ((f + 1) !)) is complex real ext-real Element of REAL
((card j) !) * ((- 1) |^ (f + 1)) is complex real ext-real Element of REAL
(((card j) !) * ((- 1) |^ (f + 1))) / ((f + 1) !) is complex real ext-real Element of REAL
(((card j) !) * ((- 1) |^ (f + 1))) * (((f + 1) !) ") is complex real ext-real set
s . (f + 1) is complex real ext-real integer set
(comega . f) + (s . (f + 1)) is complex real ext-real integer V49() Element of INT
addint . ((comega . f),(s . (f + 1))) is set
(exp_R E) * ((- 1) |^ ((card j) + 1)) is complex real ext-real Element of REAL
((exp_R E) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !) is complex real ext-real Element of REAL
((exp_R E) * ((- 1) |^ ((card j) + 1))) * ((((card j) + 1) !) ") is complex real ext-real set
((card j) !) * (((exp_R E) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !)) is complex real ext-real Element of REAL
(card (j)) + (((card j) !) * (((exp_R E) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !))) is complex real ext-real Element of REAL
((card j) !) * (exp_R (- 1)) is non empty complex real ext-real positive non negative Element of REAL
1 / (exp_R 1) is non empty complex real ext-real positive non negative Element of REAL
(exp_R 1) " is non empty complex real ext-real positive non negative set
1 * ((exp_R 1) ") is non empty complex real ext-real positive non negative set
((card j) !) * (1 / (exp_R 1)) is non empty complex real ext-real positive non negative Element of REAL
- (((card j) !) * (((exp_R E) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !))) is complex real ext-real Element of REAL
j is non empty finite set
(j) is finite set
K7(j,j) is Relation-like finite set
K6(K7(j,j)) is finite V48() set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective Element of K6(K7(j,j)) : not b₁ is with_fixpoint } is set
card (j) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
card j is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(card j) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (card j) is complex real ext-real Element of REAL
((card j) !) / number_e is non empty complex real ext-real positive non negative Element of REAL
number_e " is non empty complex real ext-real positive non negative set
((card j) !) * (number_e ") is non empty complex real ext-real positive non negative set
(card (j)) - (((card j) !) / number_e) is complex real ext-real Element of REAL
- (((card j) !) / number_e) is non empty complex real ext-real non positive negative set
(card (j)) + (- (((card j) !) / number_e)) is complex real ext-real set
|.((card (j)) - (((card j) !) / number_e)).| is complex real ext-real Element of REAL
(card j) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(- 1) |^ ((card j) + 1) is complex real ext-real set
((card j) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . ((card j) + 1) is complex real ext-real Element of REAL
s is complex real ext-real set
exp_R s is non empty complex real ext-real positive non negative set
K323(exp_R,s) is complex real ext-real Element of REAL
(exp_R s) * ((- 1) |^ ((card j) + 1)) is complex real ext-real Element of REAL
((exp_R s) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !) is complex real ext-real Element of REAL
(((card j) + 1) !) " is non empty complex real ext-real positive non negative set
((exp_R s) * ((- 1) |^ ((card j) + 1))) * ((((card j) + 1) !) ") is complex real ext-real set
((card j) !) * (((exp_R s) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !)) is complex real ext-real Element of REAL
- (((card j) !) * (((exp_R s) * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !))) is complex real ext-real Element of REAL
j is non empty finite set
(j) is finite set
K7(j,j) is Relation-like finite set
K6(K7(j,j)) is finite V48() set
{ b₁ where b₁ is Relation-like j -defined j -valued Function-like one-to-one V23(j) quasi_total onto bijective Element of K6(K7(j,j)) : not b₁ is with_fixpoint } is set
card (j) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
card j is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(card j) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (card j) is complex real ext-real Element of REAL
((card j) !) / number_e is non empty complex real ext-real positive non negative Element of REAL
number_e " is non empty complex real ext-real positive non negative set
((card j) !) * (number_e ") is non empty complex real ext-real positive non negative set
((((card j) !) / number_e)) is complex real ext-real integer set
(((card j) !) / number_e) + (1 / 2) is non empty complex real ext-real positive non negative Element of REAL
[\((((card j) !) / number_e) + (1 / 2))/] is complex real ext-real integer set
(card (j)) - (((card j) !) / number_e) is complex real ext-real Element of REAL
- (((card j) !) / number_e) is non empty complex real ext-real non positive negative set
(card (j)) + (- (((card j) !) / number_e)) is complex real ext-real set
|.((card (j)) - (((card j) !) / number_e)).| is complex real ext-real Element of REAL
({}) is finite set
{ b₁ where b₁ is Relation-like {} -defined {} -valued Function-like one-to-one V23( {} ) quasi_total onto bijective Element of K6(K7({},{})) : not b₁ is with_fixpoint } is set
{{}} is non empty V2() functional finite V48() V50() V51() V52() V53() V54() V55() 1 -element set
j is set
z is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional V23( {} ) quasi_total onto bijective ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() Element of K6(K7({},{}))
j is set
rng (id {}) is empty V2() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() V40() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V189() V193() Element of K6({})
K6({}) is finite V48() set
j is set
{j} is non empty V2() finite 1 -element set
({j}) is finite set
K7({j},{j}) is Relation-like finite set
K6(K7({j},{j})) is finite V48() set
{ b₁ where b₁ is Relation-like {j} -defined {j} -valued Function-like one-to-one V23({j}) quasi_total onto bijective Element of K6(K7({j},{j})) : not b₁ is with_fixpoint } is set
card {j} is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
1 / number_e is non empty complex real ext-real positive non negative Element of REAL
number_e " is non empty complex real ext-real positive non negative set
1 * (number_e ") is non empty complex real ext-real positive non negative set
- (1 / number_e) is non empty complex real ext-real non positive negative Element of REAL
- (1 / 2) is non empty complex real ext-real non positive negative V49() Element of RAT
0 - (1 / number_e) is non empty complex real ext-real non positive negative Element of REAL
- (1 / number_e) is non empty complex real ext-real non positive negative set
0 + (- (1 / number_e)) is non empty complex real ext-real non positive negative set
|.(0 - (1 / number_e)).| is complex real ext-real Element of REAL
((1 / number_e)) is complex real ext-real integer set
(1 / number_e) + (1 / 2) is non empty complex real ext-real positive non negative Element of REAL
[\((1 / number_e) + (1 / 2))/] is complex real ext-real integer set
card ({j}) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
K7(NAT,INT) is V2() Relation-like RAT -valued INT -valued V33() V34() V35() non finite set
K6(K7(NAT,INT)) is V2() non finite set
j is complex real ext-real integer V49() Element of INT
z is complex real ext-real integer V49() Element of INT
s is non empty Relation-like NAT -defined INT -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,INT))
s . 0 is complex real ext-real integer V49() Element of INT
s . 1 is complex real ext-real integer V49() Element of INT
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
t + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s . (t + 2) is complex real ext-real integer V49() Element of INT
t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s . t is complex real ext-real integer V49() Element of INT
s . (t + 1) is complex real ext-real integer V49() Element of INT
(s . t) + (s . (t + 1)) is complex real ext-real integer V49() Element of INT
(t + 1) * ((s . t) + (s . (t + 1))) is complex real ext-real integer V49() Element of INT
s is non empty Relation-like NAT -defined INT -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,INT))
s . 0 is complex real ext-real integer V49() Element of INT
s . 1 is complex real ext-real integer V49() Element of INT
t is non empty Relation-like NAT -defined INT -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,INT))
t . 0 is complex real ext-real integer V49() Element of INT
t . 1 is complex real ext-real integer V49() Element of INT
j is complex real ext-real integer V49() Element of INT
z is complex real ext-real integer V49() Element of INT
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
E + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s . (E + 2) is complex real ext-real integer V49() Element of INT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s . E is complex real ext-real integer V49() Element of INT
s . (E + 1) is complex real ext-real integer V49() Element of INT
(s . E) + (s . (E + 1)) is complex real ext-real integer V49() Element of INT
(E + 1) * ((s . E) + (s . (E + 1))) is complex real ext-real integer V49() Element of INT
E is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
E + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
t . (E + 2) is complex real ext-real integer V49() Element of INT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
t . E is complex real ext-real integer V49() Element of INT
t . (E + 1) is complex real ext-real integer V49() Element of INT
(t . E) + (t . (E + 1)) is complex real ext-real integer V49() Element of INT
(E + 1) * ((t . E) + (t . (E + 1))) is complex real ext-real integer V49() Element of INT
() is non empty Relation-like NAT -defined INT -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,INT))
t is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
s is complex real ext-real integer set
s (#) t is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
t is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
s is complex set
s (#) t is T-Sequence-like Relation-like NAT -defined Function-like V33() finite V193() set
s is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
Sum s is complex real ext-real integer Element of COMPLEX
len s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
(len s) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s . ((len s) -' 1) is complex real ext-real integer set
t is complex real ext-real integer set
t * (Sum s) is complex real ext-real integer V49() Element of INT
t (#) s is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
(t (#) s) | ((len s) -' 1) is T-Sequence-like Relation-like (len s) -' 1 -defined NAT -defined INT -valued rng (t (#) s) -valued Function-like V33() V34() V35() finite V193() set
rng (t (#) s) is finite V50() V51() V52() V53() V54() set
Sum ((t (#) s) | ((len s) -' 1)) is complex real ext-real integer Element of COMPLEX
t * (s . ((len s) -' 1)) is complex real ext-real integer V49() Element of INT
(Sum ((t (#) s) | ((len s) -' 1))) + (t * (s . ((len s) -' 1))) is complex real ext-real integer V49() Element of INT
((len s) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
dom (t (#) s) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
Sum (t (#) s) is complex real ext-real integer Element of COMPLEX
(t (#) s) | (len s) is T-Sequence-like Relation-like len s -defined NAT -defined INT -valued rng (t (#) s) -valued Function-like V33() V34() V35() finite V193() set
Sum ((t (#) s) | (len s)) is complex real ext-real integer Element of COMPLEX
(t (#) s) | (((len s) -' 1) + 1) is T-Sequence-like Relation-like ((len s) -' 1) + 1 -defined NAT -defined INT -valued rng (t (#) s) -valued Function-like V33() V34() V35() finite V193() set
Sum ((t (#) s) | (((len s) -' 1) + 1)) is complex real ext-real integer Element of COMPLEX
(t (#) s) . ((len s) -' 1) is complex real ext-real integer set
(Sum ((t (#) s) | ((len s) -' 1))) + ((t (#) s) . ((len s) -' 1)) is complex real ext-real integer V49() Element of INT
t is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
len t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
s is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
len s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
(len s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
t | (len s) is T-Sequence-like Relation-like len s -defined NAT -defined INT -valued rng t -valued Function-like V33() V34() V35() finite V193() set
rng t is finite V50() V51() V52() V53() V54() set
Sum t is complex real ext-real integer Element of COMPLEX
Sum s is complex real ext-real integer Element of COMPLEX
t . (len s) is complex real ext-real integer set
E is complex real ext-real integer set
E (#) s is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
E * (Sum s) is complex real ext-real integer V49() Element of INT
(E * (Sum s)) + (t . (len s)) is complex real ext-real integer V49() Element of INT
t | (len t) is T-Sequence-like Relation-like len t -defined NAT -defined INT -valued rng t -valued Function-like V33() V34() V35() finite V193() set
Sum (t | (len t)) is complex real ext-real integer Element of COMPLEX
Sum (t | (len s)) is complex real ext-real integer Element of COMPLEX
(Sum (t | (len s))) + (t . (len s)) is complex real ext-real integer V49() Element of INT
s is finite set
card s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
() . (card s) is complex real ext-real integer V49() Element of INT
(s) is finite set
K7(s,s) is Relation-like finite set
K6(K7(s,s)) is finite V48() set
{ b₁ where b₁ is Relation-like s -defined s -valued Function-like one-to-one V23(s) quasi_total onto bijective Element of K6(K7(s,s)) : not b₁ is with_fixpoint } is set
card (s) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
() . 0 is complex real ext-real integer set
t is finite set
card t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(t) is finite set
K7(t,t) is Relation-like finite set
K6(K7(t,t)) is finite V48() set
{ b₁ where b₁ is Relation-like t -defined t -valued Function-like one-to-one V23(t) quasi_total onto bijective Element of K6(K7(t,t)) : not b₁ is with_fixpoint } is set
card (t) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
() . 0 is complex real ext-real integer V49() Element of INT
() . 1 is complex real ext-real integer set
t is finite set
card t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(t) is finite set
K7(t,t) is Relation-like finite set
K6(K7(t,t)) is finite V48() set
{ b₁ where b₁ is Relation-like t -defined t -valued Function-like one-to-one V23(t) quasi_total onto bijective Element of K6(K7(t,t)) : not b₁ is with_fixpoint } is set
card (t) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
E is set
{E} is non empty V2() finite 1 -element set
() . 1 is complex real ext-real integer V49() Element of INT
card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V49() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() Element of omega
dom {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer finite finite-yielding V48() V50() V51() V52() V53() V54() V55() V56() cardinal {} -element V193() set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
() . t is complex real ext-real integer set
t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
() . (t + 1) is complex real ext-real integer set
t + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
() . (t + 2) is complex real ext-real integer set
card t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
card (t + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
K7(t,t) is Relation-like RAT -valued INT -valued V33() V34() V35() V36() finite set
K6(K7(t,t)) is finite V48() set
{ b₁ where b₁ is Relation-like t -defined t -valued Function-like V23(t) quasi_total V33() V34() V35() V36() finite Element of K6(K7(t,t)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in t or not b₁ . b₂ = b₂ ) ) ) } is set
card { b₁ where b₁ is Relation-like t -defined t -valued Function-like V23(t) quasi_total V33() V34() V35() V36() finite Element of K6(K7(t,t)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in t or not b₁ . b₂ = b₂ ) ) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
t ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . t is complex real ext-real Element of REAL
comega is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
Sum comega is complex real ext-real integer Element of COMPLEX
dom comega is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
K7((t + 1),(t + 1)) is Relation-like RAT -valued INT -valued V33() V34() V35() V36() finite set
K6(K7((t + 1),(t + 1))) is finite V48() set
{ b₁ where b₁ is non empty Relation-like t + 1 -defined t + 1 -valued Function-like V23(t + 1) quasi_total V33() V34() V35() V36() finite Element of K6(K7((t + 1),(t + 1))) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in t + 1 or not b₁ . b₂ = b₂ ) ) ) } is set
card { b₁ where b₁ is non empty Relation-like t + 1 -defined t + 1 -valued Function-like V23(t + 1) quasi_total V33() V34() V35() V36() finite Element of K6(K7((t + 1),(t + 1))) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in t + 1 or not b₁ . b₂ = b₂ ) ) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
(t + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(t + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (t + 1) is complex real ext-real Element of REAL
f is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
Sum f is complex real ext-real integer Element of COMPLEX
dom f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
(t) is finite set
{ b₁ where b₁ is Relation-like t -defined t -valued Function-like one-to-one V23(t) quasi_total onto bijective Element of K6(K7(t,t)) : not b₁ is with_fixpoint } is set
card (t) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
() . t is complex real ext-real integer V49() Element of INT
((t + 1)) is finite set
{ b₁ where b₁ is Relation-like t + 1 -defined t + 1 -valued Function-like one-to-one V23(t + 1) quasi_total onto bijective Element of K6(K7((t + 1),(t + 1))) : not b₁ is with_fixpoint } is set
card ((t + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
() . (t + 1) is complex real ext-real integer V49() Element of INT
sn2 is finite set
card sn2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(sn2) is finite set
K7(sn2,sn2) is Relation-like finite set
K6(K7(sn2,sn2)) is finite V48() set
{ b₁ where b₁ is Relation-like sn2 -defined sn2 -valued Function-like one-to-one V23(sn2) quasi_total onto bijective Element of K6(K7(sn2,sn2)) : not b₁ is with_fixpoint } is set
card (sn2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
{ b₁ where b₁ is Relation-like sn2 -defined sn2 -valued Function-like V23(sn2) quasi_total finite Element of K6(K7(sn2,sn2)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in sn2 or not b₁ . b₂ = b₂ ) ) ) } is set
card { b₁ where b₁ is Relation-like sn2 -defined sn2 -valued Function-like V23(sn2) quasi_total finite Element of K6(K7(sn2,sn2)) : ( b₁ is one-to-one & ( for b₂ being set holds
( not b₂ in sn2 or not b₁ . b₂ = b₂ ) ) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
(t + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(t + 2) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (t + 2) is complex real ext-real Element of REAL
XFn2 is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
Sum XFn2 is complex real ext-real integer Element of COMPLEX
dom XFn2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
len comega is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom comega is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
(len comega) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
len XFn2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom XFn2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal set
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(t + 1) (#) comega is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
dom ((t + 1) (#) comega) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
a is set
f | (len comega) is T-Sequence-like Relation-like len comega -defined NAT -defined INT -valued rng f -valued Function-like V33() V34() V35() finite V193() set
rng f is finite V50() V51() V52() V53() V54() set
dom (f | (len comega)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(f | (len comega)) . a is complex real ext-real integer set
f . a is complex real ext-real integer set
(- 1) |^ x is complex real ext-real set
((- 1) |^ x) * ((t + 1) !) is complex real ext-real Element of REAL
x ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . x is complex real ext-real Element of REAL
(((- 1) |^ x) * ((t + 1) !)) / (x !) is complex real ext-real Element of REAL
(x !) " is non empty complex real ext-real positive non negative set
(((- 1) |^ x) * ((t + 1) !)) * ((x !) ") is complex real ext-real set
(t !) * (t + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((- 1) |^ x) * ((t !) * (t + 1)) is complex real ext-real Element of REAL
(((- 1) |^ x) * ((t !) * (t + 1))) / (x !) is complex real ext-real Element of REAL
(((- 1) |^ x) * ((t !) * (t + 1))) * ((x !) ") is complex real ext-real set
((- 1) |^ x) * (t !) is complex real ext-real Element of REAL
(((- 1) |^ x) * (t !)) / (x !) is complex real ext-real Element of REAL
(((- 1) |^ x) * (t !)) * ((x !) ") is complex real ext-real set
(t + 1) * ((((- 1) |^ x) * (t !)) / (x !)) is complex real ext-real Element of REAL
comega . x is complex real ext-real integer set
(t + 1) * (comega . x) is complex real ext-real integer V49() Element of INT
((t + 1) (#) comega) . a is complex real ext-real integer set
(- 1) |^ (t + 1) is complex real ext-real set
(- 1) * ((- 1) |^ (t + 1)) is complex real ext-real Element of REAL
(- 1) |^ ((t + 1) + 1) is complex real ext-real set
(t + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(t + 2) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(t + 1) * (Sum comega) is complex real ext-real integer V49() Element of INT
f . (len comega) is complex real ext-real integer set
((t + 1) * (Sum comega)) + (f . (len comega)) is complex real ext-real integer V49() Element of INT
((- 1) |^ (t + 1)) * ((t + 1) !) is complex real ext-real Element of REAL
(((- 1) |^ (t + 1)) * ((t + 1) !)) / ((t + 1) !) is complex real ext-real Element of REAL
((t + 1) !) " is non empty complex real ext-real positive non negative set
(((- 1) |^ (t + 1)) * ((t + 1) !)) * (((t + 1) !) ") is complex real ext-real set
((t + 1) * (Sum comega)) + ((((- 1) |^ (t + 1)) * ((t + 1) !)) / ((t + 1) !)) is complex real ext-real Element of REAL
((t + 1) !) / ((t + 1) !) is non empty complex real ext-real positive non negative Element of REAL
((t + 1) !) * (((t + 1) !) ") is non empty complex real ext-real positive non negative set
((- 1) |^ (t + 1)) * (((t + 1) !) / ((t + 1) !)) is complex real ext-real Element of REAL
((t + 1) * (Sum comega)) + (((- 1) |^ (t + 1)) * (((t + 1) !) / ((t + 1) !))) is complex real ext-real Element of REAL
((- 1) |^ (t + 1)) * 1 is complex real ext-real Element of REAL
((t + 1) * (Sum comega)) + (((- 1) |^ (t + 1)) * 1) is complex real ext-real Element of REAL
x is set
XFn2 | (len f) is T-Sequence-like Relation-like len f -defined NAT -defined INT -valued rng XFn2 -valued Function-like V33() V34() V35() finite V193() set
rng XFn2 is finite V50() V51() V52() V53() V54() set
dom (XFn2 | (len f)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(XFn2 | (len f)) . x is complex real ext-real integer set
XFn2 . x is complex real ext-real integer set
(- 1) |^ m is complex real ext-real set
((t + 1) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . ((t + 1) + 1) is complex real ext-real Element of REAL
((- 1) |^ m) * (((t + 1) + 1) !) is complex real ext-real Element of REAL
m ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . m is complex real ext-real Element of REAL
(((- 1) |^ m) * (((t + 1) + 1) !)) / (m !) is complex real ext-real Element of REAL
(m !) " is non empty complex real ext-real positive non negative set
(((- 1) |^ m) * (((t + 1) + 1) !)) * ((m !) ") is complex real ext-real set
((t + 1) !) * ((t + 1) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((- 1) |^ m) * (((t + 1) !) * ((t + 1) + 1)) is complex real ext-real Element of REAL
(((- 1) |^ m) * (((t + 1) !) * ((t + 1) + 1))) / (m !) is complex real ext-real Element of REAL
(((- 1) |^ m) * (((t + 1) !) * ((t + 1) + 1))) * ((m !) ") is complex real ext-real set
((- 1) |^ m) * ((t + 1) !) is complex real ext-real Element of REAL
(((- 1) |^ m) * ((t + 1) !)) / (m !) is complex real ext-real Element of REAL
(((- 1) |^ m) * ((t + 1) !)) * ((m !) ") is complex real ext-real set
((t + 1) + 1) * ((((- 1) |^ m) * ((t + 1) !)) / (m !)) is complex real ext-real Element of REAL
f . m is complex real ext-real integer set
(t + 2) * (f . m) is complex real ext-real integer V49() Element of INT
(t + 2) (#) f is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V33() V34() V35() finite V193() set
((t + 2) (#) f) . x is complex real ext-real integer set
t + 3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom ((t + 2) (#) f) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of K6(NAT)
(t + 2) * (Sum f) is complex real ext-real integer V49() Element of INT
XFn2 . (len f) is complex real ext-real integer set
((t + 2) * (Sum f)) + (XFn2 . (len f)) is complex real ext-real integer V49() Element of INT
(- 1) |^ (t + 2) is complex real ext-real set
((- 1) |^ (t + 2)) * ((t + 2) !) is complex real ext-real Element of REAL
(((- 1) |^ (t + 2)) * ((t + 2) !)) / ((t + 2) !) is complex real ext-real Element of REAL
((t + 2) !) " is non empty complex real ext-real positive non negative set
(((- 1) |^ (t + 2)) * ((t + 2) !)) * (((t + 2) !) ") is complex real ext-real set
((t + 2) * (Sum f)) + ((((- 1) |^ (t + 2)) * ((t + 2) !)) / ((t + 2) !)) is complex real ext-real Element of REAL
- ((- 1) |^ (t + 1)) is complex real ext-real Element of REAL
((t + 2) !) / ((t + 2) !) is non empty complex real ext-real positive non negative Element of REAL
((t + 2) !) * (((t + 2) !) ") is non empty complex real ext-real positive non negative set
(- ((- 1) |^ (t + 1))) * (((t + 2) !) / ((t + 2) !)) is complex real ext-real Element of REAL
((t + 2) * (Sum f)) + ((- ((- 1) |^ (t + 1))) * (((t + 2) !) / ((t + 2) !))) is complex real ext-real Element of REAL
(- ((- 1) |^ (t + 1))) * 1 is complex real ext-real Element of REAL
((t + 2) * (Sum f)) + ((- ((- 1) |^ (t + 1))) * 1) is complex real ext-real Element of REAL
(Sum comega) + (Sum f) is complex real ext-real integer V49() Element of INT
(t + 1) * ((Sum comega) + (Sum f)) is complex real ext-real integer V49() Element of INT
() . (t + 2) is complex real ext-real integer V49() Element of INT
s is set
t is set
K7(s,t) is Relation-like set
K6(K7(s,t)) is set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t)) : not b₁ is one-to-one } is set
Funcs (s,t) is functional set
K6((Funcs (s,t))) is set
E is set
comega is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t))
E is set
comega is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t))
s is finite set
t is finite set
(s,t) is functional finite Element of K6((Funcs (s,t)))
Funcs (s,t) is functional finite set
K6((Funcs (s,t))) is finite V48() set
K7(s,t) is Relation-like finite set
K6(K7(s,t)) is finite V48() set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t)) : not b₁ is one-to-one } is set
F₂() is set
F₁() is set
K7(F₁(),F₂()) is Relation-like set
K6(K7(F₁(),F₂())) is set
{ b₁ where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of K6(K7(F₁(),F₂())) : P₁[b₁] } is set
Funcs (F₁(),F₂()) is functional set
{ b₁ where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of K6(K7(F₁(),F₂())) : P₁[b₁] } is set
(Funcs (F₁(),F₂())) \ { b₁ where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of K6(K7(F₁(),F₂())) : P₁[b₁] } is functional Element of K6((Funcs (F₁(),F₂())))
K6((Funcs (F₁(),F₂()))) is set
comega is set
f is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of K6(K7(F₁(),F₂()))
sn2 is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of K6(K7(F₁(),F₂()))
comega is set
s is finite set
card s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
t is finite set
card t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(s,t) is functional finite Element of K6((Funcs (s,t)))
Funcs (s,t) is functional finite set
K6((Funcs (s,t))) is finite V48() set
K7(s,t) is Relation-like finite set
K6(K7(s,t)) is finite V48() set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t)) : not b₁ is one-to-one } is set
card (s,t) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(card t) |^ (card s) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(card t) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (card t) is complex real ext-real Element of REAL
(card t) -' (card s) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((card t) -' (card s)) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . ((card t) -' (card s)) is complex real ext-real Element of REAL
((card t) !) / (((card t) -' (card s)) !) is non empty complex real ext-real positive non negative Element of REAL
(((card t) -' (card s)) !) " is non empty complex real ext-real positive non negative set
((card t) !) * ((((card t) -' (card s)) !) ") is non empty complex real ext-real positive non negative set
((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) is complex real ext-real Element of REAL
- (((card t) !) / (((card t) -' (card s)) !)) is non empty complex real ext-real non positive negative set
((card t) |^ (card s)) + (- (((card t) !) / (((card t) -' (card s)) !))) is complex real ext-real set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total finite Element of K6(K7(s,t)) : b₁ is one-to-one } is set
comega is set
f is Relation-like s -defined t -valued Function-like quasi_total finite Element of K6(K7(s,t))
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total finite Element of K6(K7(s,t)) : not S₁[b₁] } is set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total finite Element of K6(K7(s,t)) : S₁[b₁] } is set
(Funcs (s,t)) \ { b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total finite Element of K6(K7(s,t)) : S₁[b₁] } is functional finite Element of K6((Funcs (s,t)))
card (Funcs (s,t)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
comega is functional finite Element of K6((Funcs (s,t)))
card comega is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(card (Funcs (s,t))) - (card comega) is complex real ext-real integer V49() Element of INT
- (card comega) is complex real ext-real non positive integer set
(card (Funcs (s,t))) + (- (card comega)) is complex real ext-real integer set
(card (Funcs (s,t))) - (((card t) !) / (((card t) -' (card s)) !)) is complex real ext-real Element of REAL
(card (Funcs (s,t))) + (- (((card t) !) / (((card t) -' (card s)) !))) is complex real ext-real set
365 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
23 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 23 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 365 is complex real ext-real Element of REAL
365 -' 23 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 -' 23) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (365 -' 23) is complex real ext-real Element of REAL
(365 !) / ((365 -' 23) !) is non empty complex real ext-real positive non negative Element of REAL
((365 -' 23) !) " is non empty complex real ext-real positive non negative set
(365 !) * (((365 -' 23) !) ") is non empty complex real ext-real positive non negative set
(365 |^ 23) - ((365 !) / ((365 -' 23) !)) is complex real ext-real Element of REAL
- ((365 !) / ((365 -' 23) !)) is non empty complex real ext-real non positive negative set
(365 |^ 23) + (- ((365 !) / ((365 -' 23) !))) is complex real ext-real set
2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) is complex real ext-real Element of REAL
364 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
364 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(364 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (364 + 1) is complex real ext-real Element of REAL
364 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 364 is complex real ext-real Element of REAL
(364 !) * (364 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
363 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
363 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(363 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (363 + 1) is complex real ext-real Element of REAL
363 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 363 is complex real ext-real Element of REAL
(363 !) * (363 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
362 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
362 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(362 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (362 + 1) is complex real ext-real Element of REAL
362 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 362 is complex real ext-real Element of REAL
(362 !) * (362 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
361 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
361 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(361 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (361 + 1) is complex real ext-real Element of REAL
361 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 361 is complex real ext-real Element of REAL
(361 !) * (361 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
360 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
360 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(360 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (360 + 1) is complex real ext-real Element of REAL
360 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 360 is complex real ext-real Element of REAL
(360 !) * (360 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
359 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
359 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(359 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (359 + 1) is complex real ext-real Element of REAL
359 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 359 is complex real ext-real Element of REAL
(359 !) * (359 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
358 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
358 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(358 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (358 + 1) is complex real ext-real Element of REAL
358 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 358 is complex real ext-real Element of REAL
(358 !) * (358 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
357 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
357 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(357 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (357 + 1) is complex real ext-real Element of REAL
357 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 357 is complex real ext-real Element of REAL
(357 !) * (357 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
356 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
356 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(356 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (356 + 1) is complex real ext-real Element of REAL
356 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 356 is complex real ext-real Element of REAL
(356 !) * (356 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
355 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
355 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(355 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (355 + 1) is complex real ext-real Element of REAL
355 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 355 is complex real ext-real Element of REAL
(355 !) * (355 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
354 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
354 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(354 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (354 + 1) is complex real ext-real Element of REAL
354 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 354 is complex real ext-real Element of REAL
(354 !) * (354 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
353 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
353 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(353 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (353 + 1) is complex real ext-real Element of REAL
353 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 353 is complex real ext-real Element of REAL
(353 !) * (353 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
352 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
352 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(352 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (352 + 1) is complex real ext-real Element of REAL
352 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 352 is complex real ext-real Element of REAL
(352 !) * (352 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
351 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
351 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(351 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (351 + 1) is complex real ext-real Element of REAL
351 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 351 is complex real ext-real Element of REAL
(351 !) * (351 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
350 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
350 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(350 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (350 + 1) is complex real ext-real Element of REAL
350 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 350 is complex real ext-real Element of REAL
(350 !) * (350 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
349 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
349 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(349 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (349 + 1) is complex real ext-real Element of REAL
349 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 349 is complex real ext-real Element of REAL
(349 !) * (349 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
348 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
348 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(348 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (348 + 1) is complex real ext-real Element of REAL
348 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 348 is complex real ext-real Element of REAL
(348 !) * (348 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
347 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
347 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(347 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (347 + 1) is complex real ext-real Element of REAL
347 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 347 is complex real ext-real Element of REAL
(347 !) * (347 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
346 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
346 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(346 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (346 + 1) is complex real ext-real Element of REAL
346 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 346 is complex real ext-real Element of REAL
(346 !) * (346 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
345 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
345 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(345 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (345 + 1) is complex real ext-real Element of REAL
345 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 345 is complex real ext-real Element of REAL
(345 !) * (345 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
344 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
344 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(344 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (344 + 1) is complex real ext-real Element of REAL
344 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 344 is complex real ext-real Element of REAL
(344 !) * (344 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
343 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
343 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(343 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (343 + 1) is complex real ext-real Element of REAL
343 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 343 is complex real ext-real Element of REAL
(343 !) * (343 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
342 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
342 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(342 + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . (342 + 1) is complex real ext-real Element of REAL
342 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V50() V51() V52() V53() V54() V55() cardinal Element of REAL
Prod_real_n . 342 is complex real ext-real Element of REAL
(342 !) * (342 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 * 364 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 * 364) * 363 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((365 * 364) * 363) * 362 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((365 * 364) * 363) * 362) * 361 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((((365 * 364) * 363) * 362) * 361) * 360 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
359 * 358 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(359 * 358) * 357 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((359 * 358) * 357) * 356 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((359 * 358) * 357) * 356) * 355 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((((359 * 358) * 357) * 356) * 355) * 354 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((((359 * 358) * 357) * 356) * 355) * 354) * 353 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
352 * 351 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(352 * 351) * 350 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((352 * 351) * 350) * 349 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((352 * 351) * 350) * 349) * 348 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((((352 * 351) * 350) * 349) * 348) * 347 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((((352 * 351) * 350) * 349) * 348) * 347) * 346 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343)) * (342 !) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 !) / (342 !) is non empty complex real ext-real positive non negative Element of REAL
(342 !) " is non empty complex real ext-real positive non negative set
(365 !) * ((342 !) ") is non empty complex real ext-real positive non negative set
365 |^ 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 * 365 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (2 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 * 365) * 365 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
3 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (3 + 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 |^ 3) * (365 |^ 2) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
3 + 3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (3 + 3) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 |^ 3) * (365 |^ 3) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
6 + 5 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (6 + 5) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 6 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 |^ 6) * (365 |^ 5) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
6 + 6 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (6 + 6) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 |^ 6) * (365 |^ 6) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
12 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
11 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
12 + 11 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ (12 + 11) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 12 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
365 |^ 11 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 |^ 12) * (365 |^ 11) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(365 |^ 23) - ((365 !) / (342 !)) is complex real ext-real Element of REAL
- ((365 !) / (342 !)) is non empty complex real ext-real non positive negative set
(365 |^ 23) + (- ((365 !) / (342 !))) is complex real ext-real set
2 * ((365 |^ 23) - ((365 !) / (342 !))) is complex real ext-real Element of REAL
365 - 23 is complex real ext-real integer V49() Element of INT
- 23 is non empty complex real ext-real non positive negative integer set
365 + (- 23) is complex real ext-real integer set
s is finite set
card s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
t is non empty finite set
card t is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
(s,t) is functional finite Element of K6((Funcs (s,t)))
Funcs (s,t) is non empty functional finite set
K6((Funcs (s,t))) is finite V48() set
K7(s,t) is Relation-like finite set
K6(K7(s,t)) is finite V48() set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t)) : not b₁ is one-to-one } is set
card (s,t) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
2 * (card (s,t)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
Funcs (s,t) is non empty functional finite FUNCTION_DOMAIN of s,t
card (Funcs (s,t)) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
s is non empty finite set
card s is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
t is non empty finite set
card t is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
Funcs (s,t) is non empty functional finite set
(s,t) is functional finite Element of K6((Funcs (s,t)))
K6((Funcs (s,t))) is finite V48() set
K7(s,t) is Relation-like finite set
K6(K7(s,t)) is finite V48() set
{ b₁ where b₁ is Relation-like s -defined t -valued Function-like quasi_total Element of K6(K7(s,t)) : not b₁ is one-to-one } is set
prob (s,t) is complex real ext-real Element of REAL
Funcs (s,t) is non empty functional finite FUNCTION_DOMAIN of s,t
card (Funcs (s,t)) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
card (s,t) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of omega
2 * (card (s,t)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite V49() V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(2 * (card (s,t))) / 2 is complex real ext-real non negative V49() Element of RAT
(2 * (card (s,t))) * (2 ") is complex real ext-real non negative set
(card (Funcs (s,t))) / 2 is non empty complex real ext-real positive non negative V49() Element of RAT
(card (Funcs (s,t))) * (2 ") is non empty complex real ext-real positive non negative set
(card (s,t)) / (card (Funcs (s,t))) is complex real ext-real non negative V49() Element of RAT
(card (Funcs (s,t))) " is non empty complex real ext-real positive non negative set
(card (s,t)) * ((card (Funcs (s,t))) ") is complex real ext-real non negative set
((card (Funcs (s,t))) / 2) / (card (Funcs (s,t))) is non empty complex real ext-real positive non negative V49() Element of RAT
((card (Funcs (s,t))) / 2) * ((card (Funcs (s,t))) ") is non empty complex real ext-real positive non negative set
(card (Funcs (s,t))) / (card (Funcs (s,t))) is non empty complex real ext-real positive non negative V49() Element of RAT
(card (Funcs (s,t))) * ((card (Funcs (s,t))) ") is non empty complex real ext-real positive non negative set
((card (Funcs (s,t))) / (card (Funcs (s,t)))) / 2 is non empty complex real ext-real positive non negative V49() Element of RAT
((card (Funcs (s,t))) / (card (Funcs (s,t)))) * (2 ") is non empty complex real ext-real positive non negative set