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

{{},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

- 1 is non empty complex real ext-real non positive negative integer V49() Element of INT

dom exp_R is non empty V50() V51() V52() Element of K6(REAL)

- 1 is non empty complex real ext-real non positive negative integer set
Funcs ({},{}) is non empty functional finite set

{()} is non empty V2() functional finite V48() V50() V51() V52() V53() V54() V55() 1 -element set

K6(K7({},{})) is finite V48() set
j is set

exp_R j is non empty complex real ext-real positive non negative 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 + (1 / 2) is complex real ext-real Element of REAL
[\(j + (1 / 2))/] 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 + (1 / 2)) - 1 is complex real ext-real Element of REAL
(j + (1 / 2)) + (- 1) 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 + (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 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)

].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

Taylor (exp_R,(),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,(),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,(),s,z))) . j is complex real ext-real Element of REAL

z + (- s) is complex real ext-real set
(z - s) |^ (j + 1) is complex real ext-real Element of REAL

(diff (exp_R,())) . j is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))

[.z,s.] is V50() V51() V52() V84() Element of K6(REAL)
((diff (exp_R,())) . 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))

(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,(),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,(),s,z))) . j) + (((exp_R comega) * ((z - s) |^ (j + 1))) / ((j + 1) !)) is complex real ext-real Element of REAL

(- 1) |^ (j + 1) is complex real ext-real set

exp_R z is non empty complex real ext-real positive non negative set

() * ((- 1) |^ (j + 1)) is complex real ext-real Element of REAL
(() * ((- 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
(() * ((- 1) |^ (j + 1))) * (((j + 1) !) ") is complex real ext-real set
(j !) * ((() * ((- 1) |^ (j + 1))) / ((j + 1) !)) is complex real ext-real Element of REAL
- ((j !) * ((() * ((- 1) |^ (j + 1))) / ((j + 1) !))) is complex real ext-real Element of REAL
|.(- ((j !) * ((() * ((- 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 Element of REAL
(j + 1) " is non empty complex real ext-real positive non negative set
() * ((j + 1) ") is non empty complex real ext-real positive non negative set
() / 2 is non empty complex real ext-real positive non negative Element of REAL
() * (2 ") is non empty complex real ext-real positive non negative set
(- 1) |^ j is complex real ext-real set
() * ((- 1) |^ j) is complex real ext-real Element of REAL
(() * ((- 1) |^ j)) / (j + 1) is complex real ext-real Element of REAL
(() * ((- 1) |^ j)) * ((j + 1) ") is complex real ext-real set
|.((() * ((- 1) |^ j)) / (j + 1)).| is complex real ext-real Element of REAL

- (1 / 2) is non empty complex real ext-real non positive negative V49() Element of RAT

- (() / (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
() * ((- 1) * (((- 1) |^ j) * (- 1))) is complex real ext-real Element of REAL
(() * ((- 1) * (((- 1) |^ j) * (- 1)))) / (j + 1) is complex real ext-real Element of REAL
(() * ((- 1) * (((- 1) |^ j) * (- 1)))) * ((j + 1) ") is complex real ext-real set
(- 1) * ((- 1) |^ (j + 1)) is complex real ext-real Element of REAL
() * ((- 1) * ((- 1) |^ (j + 1))) is complex real ext-real Element of REAL
(() * ((- 1) * ((- 1) |^ (j + 1)))) / (j + 1) is complex real ext-real Element of REAL
(() * ((- 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
(() * ((- 1) |^ (j + 1))) * (1 / (j + 1)) is complex real ext-real Element of REAL
- ((() * ((- 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
(() * ((- 1) |^ (j + 1))) * (((j !) / (j !)) / (j + 1)) is complex real ext-real Element of REAL
- ((() * ((- 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
(() * ((- 1) |^ (j + 1))) * ((j !) / ((j !) * (j + 1))) is complex real ext-real Element of REAL
- ((() * ((- 1) |^ (j + 1))) * ((j !) / ((j !) * (j + 1)))) is complex real ext-real Element of REAL
(() * ((- 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
((() * ((- 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
((() * ((- 1) |^ (j + 1))) * (j !)) * (((j + 1) * (j !)) ") is complex real ext-real set
- (((() * ((- 1) |^ (j + 1))) * (j !)) / ((j + 1) * (j !))) is complex real ext-real Element of REAL
(j !) * () is non empty complex real ext-real positive non negative Element of REAL
((j !) * ()) * ((- 1) |^ (j + 1)) is complex real ext-real Element of REAL
(((j !) * ()) * ((- 1) |^ (j + 1))) / ((j + 1) !) is complex real ext-real Element of REAL
(((j !) * ()) * ((- 1) |^ (j + 1))) * (((j + 1) !) ") is complex real ext-real set
- ((((j !) * ()) * ((- 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
{ b1 where b1 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 b1 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
{ b1 where b1 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 b1 is with_fixpoint } is set
{ b1 where b1 is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : b1 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 { b1 where b1 is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : b1 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

z is 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
{ b1 where b1 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 b1 is with_fixpoint } is set
{ b1 where b1 is Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : ( b1 is one-to-one & ( for b2 being set holds
( not b2 in j or not b1 . b2 = b2 ) ) )
}
is set

s is set

E is set
t . E is set
s is set

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
{ b1 where b1 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 b1 is with_fixpoint } is set

((card j) !) / number_e is non empty complex real ext-real positive non negative Element of REAL

((card j) !) * () 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

(- 1) |^ ((card j) + 1) is complex real ext-real set

Prod_real_n . ((card j) + 1) is complex real ext-real Element of REAL
{ b1 where b1 is non empty Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : ( b1 is one-to-one & ( for b2 being set holds
( not b2 in j or not b1 . b2 = b2 ) ) )
}
is set

card { b1 where b1 is non empty Relation-like j -defined j -valued Function-like V23(j) quasi_total finite Element of K6(K7(j,j)) : ( b1 is one-to-one & ( for b2 being set holds
( not b2 in j or not b1 . b2 = b2 ) ) )
}
is epsilon-transitive epsilon-connected ordinal cardinal set

Taylor (exp_R,(),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,(),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,(),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

(- 1) + () is non empty complex real ext-real non positive negative integer set
((- 1) - 0) |^ ((card j) + 1) is complex real ext-real set

exp_R E is non empty complex real ext-real positive non negative set

() * (((- 1) - 0) |^ ((card j) + 1)) is complex real ext-real Element of REAL
(() * (((- 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
(() * (((- 1) - 0) |^ ((card j) + 1))) * ((((card j) + 1) !) ") is complex real ext-real set
((Partial_Sums (Taylor (exp_R,(),0,(- 1)))) . (card j)) + ((() * (((- 1) - 0) |^ ((card j) + 1))) / (((card j) + 1) !)) is complex real ext-real Element of REAL
((card j) !) (#) (Taylor (exp_R,(),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,(),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,(),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,(),0,(- 1))))) . (card j) is complex real ext-real Element of REAL
((card j) !) * ((Partial_Sums (Taylor (exp_R,(),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

(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,(),0,(- 1))))) . 0 is complex real ext-real Element of REAL
(((card j) !) (#) (Taylor (exp_R,(),0,(- 1)))) . 0 is complex real ext-real Element of REAL
(Taylor (exp_R,(),0,(- 1))) . 0 is complex real ext-real Element of REAL
((card j) !) * ((Taylor (exp_R,(),0,(- 1))) . 0) is complex real ext-real Element of REAL

(diff (exp_R,())) . 0 is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,())) . 0) . 0 is complex real ext-real set
((- 1) - 0) |^ 0 is complex real ext-real set
(((diff (exp_R,())) . 0) . 0) * (((- 1) - 0) |^ 0) is complex real ext-real Element of REAL

((((diff (exp_R,())) . 0) . 0) * (((- 1) - 0) |^ 0)) / () is complex real ext-real Element of REAL
() " is non empty complex real ext-real positive non negative set
((((diff (exp_R,())) . 0) . 0) * (((- 1) - 0) |^ 0)) * (() ") is complex real ext-real set
((card j) !) * (((((diff (exp_R,())) . 0) . 0) * (((- 1) - 0) |^ 0)) / ()) is complex real ext-real Element of REAL

1 * ((- 1) |^ 0) is complex real ext-real Element of REAL
(1 * ((- 1) |^ 0)) / () is complex real ext-real Element of REAL
(1 * ((- 1) |^ 0)) * (() ") is complex real ext-real set
((card j) !) * ((1 * ((- 1) |^ 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)) / () is complex real ext-real Element of REAL
(((card j) !) * ((- 1) |^ 0)) * (() ") is complex real ext-real set

(Partial_Sums (((card j) !) (#) (Taylor (exp_R,(),0,(- 1))))) . f is complex real ext-real Element of REAL
comega . f is complex real ext-real integer V49() Element of INT

(Partial_Sums (((card j) !) (#) (Taylor (exp_R,(),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,(),0,(- 1)))) . (f + 1) is complex real ext-real Element of REAL
(Taylor (exp_R,(),0,(- 1))) . (f + 1) is complex real ext-real Element of REAL
((card j) !) * ((Taylor (exp_R,(),0,(- 1))) . (f + 1)) is complex real ext-real Element of REAL

(diff (exp_R,())) . (f + 1) is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,())) . (f + 1)) . 0 is complex real ext-real set
((- 1) - 0) |^ (f + 1) is complex real ext-real set
(((diff (exp_R,())) . (f + 1)) . 0) * (((- 1) - 0) |^ (f + 1)) is complex real ext-real Element of REAL

((((diff (exp_R,())) . (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,())) . (f + 1)) . 0) * (((- 1) - 0) |^ (f + 1))) * (((f + 1) !) ") is complex real ext-real set
((card j) !) * (((((diff (exp_R,())) . (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
() * ((- 1) |^ ((card j) + 1)) is complex real ext-real Element of REAL
(() * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !) is complex real ext-real Element of REAL
(() * ((- 1) |^ ((card j) + 1))) * ((((card j) + 1) !) ") is complex real ext-real set
((card j) !) * ((() * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !)) is complex real ext-real Element of REAL
(card (j)) + (((card j) !) * ((() * ((- 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 / () is non empty complex real ext-real positive non negative Element of REAL
() " is non empty complex real ext-real positive non negative set
1 * (() ") is non empty complex real ext-real positive non negative set
((card j) !) * (1 / ()) is non empty complex real ext-real positive non negative Element of REAL
- (((card j) !) * ((() * ((- 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
{ b1 where b1 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 b1 is with_fixpoint } is set

((card j) !) / number_e is non empty complex real ext-real positive non negative Element of REAL

((card j) !) * () 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

(- 1) |^ ((card j) + 1) is complex real ext-real set

Prod_real_n . ((card j) + 1) is complex real ext-real Element of REAL

exp_R s is non empty complex real ext-real positive non negative set

() * ((- 1) |^ ((card j) + 1)) is complex real ext-real Element of REAL
(() * ((- 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
(() * ((- 1) |^ ((card j) + 1))) * ((((card j) + 1) !) ") is complex real ext-real set
((card j) !) * ((() * ((- 1) |^ ((card j) + 1))) / (((card j) + 1) !)) is complex real ext-real Element of REAL
- (((card j) !) * ((() * ((- 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
{ b1 where b1 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 b1 is with_fixpoint } is set

((card j) !) / number_e is non empty complex real ext-real positive non negative Element of REAL

((card j) !) * () 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
{ b1 where b1 is Relation-like {} -defined {} -valued Function-like one-to-one V23( {} ) quasi_total onto bijective Element of K6(K7({},{})) : not b1 is with_fixpoint } is set
is non empty V2() functional finite V48() V50() V51() V52() V53() V54() V55() 1 -element set
j is set

j is set

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
{ b1 where b1 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 b1 is with_fixpoint } is set

1 * () is non empty complex real ext-real positive non negative set
- () 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 - () is non empty complex real ext-real non positive negative Element of REAL
- () is non empty complex real ext-real non positive negative set
0 + (- ()) is non empty complex real ext-real non positive negative set
|.(0 - ()).| is complex real ext-real Element of REAL
(()) is complex real ext-real integer set
() + (1 / 2) is non empty complex real ext-real positive non negative Element of REAL
[\(() + (1 / 2))/] is complex real ext-real integer set

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 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 . (t + 2) 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))

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))

s . (E + 2) 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

t . (E + 2) 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))

s is complex set

s . ((len s) -' 1) is complex real ext-real integer set

t * (Sum s) is complex real ext-real integer V49() Element of INT

(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

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

rng t is finite V50() V51() V52() V53() V54() 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

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 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
{ b1 where b1 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 b1 is with_fixpoint } is set

t is finite set

(t) is finite set
K7(t,t) is Relation-like finite set
K6(K7(t,t)) is finite V48() set
{ b1 where b1 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 b1 is with_fixpoint } is set

t is finite set

(t) is finite set
K7(t,t) is Relation-like finite set
K6(K7(t,t)) is finite V48() set
{ b1 where b1 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 b1 is with_fixpoint } is set

E is set
{E} is non empty V2() finite 1 -element set
() . 1 is complex real ext-real integer V49() Element of INT

() . (t + 1) is complex real ext-real integer set

() . (t + 2) is complex real ext-real integer set