REAL is non empty non trivial non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable Element of K10(REAL)
K10(REAL) is non empty non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable set
K10(omega) is non empty non trivial non finite set
K135() is set
K10(NAT) is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
{{}} is non empty trivial functional finite V36() 1 -element empty-membered with_common_domain countable set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative finite cardinal real integer countable Element of NAT
{} * is non empty functional V36() FinSequence-membered FinSequenceSet of {}
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
K11({{}},NAT) is non empty non trivial Relation-like non finite set
[{},{}] is set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
K11({{}},NAT) \ {[{},{}]} is non empty non trivial Relation-like {{}} -defined NAT -valued non finite Element of K10(K11({{}},NAT))
K10(K11({{}},NAT)) is non empty non trivial non finite set
K11({{}},NAT) typed\ {[{},{}]} is Relation-like {{}} -defined NAT -valued Element of K10(K11({{}},NAT))
NAT \/ (K11({{}},NAT) \ {[{},{}]}) is non empty non trivial non finite set
K11(REAL,REAL) is non empty non trivial Relation-like non finite set
K10(K11(REAL,REAL)) is non empty non trivial non finite set
K293() is non empty V75() L8()
the carrier of K293() is non empty set
<REAL,+> is non empty L8()
K299() is non empty V75() SubStr of <REAL,+>
<NAT,+> is non empty V75() V97() uniquely-decomposable SubStr of K299()
<REAL,*> is non empty V75() V97() associative commutative L8()
<NAT,*> is non empty V75() V97() uniquely-decomposable SubStr of <REAL,*>
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative finite cardinal real integer countable Element of NAT
{{},1} is non empty finite V36() countable set
K554() is set
K11(COMPLEX,COMPLEX) is non empty non trivial Relation-like non finite set
K10(K11(COMPLEX,COMPLEX)) is non empty non trivial non finite set
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative finite cardinal real integer countable Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support Element of NAT
S is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
abs S is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative finite cardinal real integer countable Element of NAT
X is complex ext-real real integer set
- 1 is non empty complex ext-real non positive negative real integer set
S is complex ext-real real integer set
S is non empty non degenerated non trivial ZeroOneStr
the carrier of S is non empty non trivial set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S \ { the OneF of S} is Element of K10( the carrier of S)
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the ZeroF of S is Element of the carrier of S
0. S is zero Element of the carrier of S
1. S is non zero Element of the carrier of S
S is ()
the carrier of S is set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is Relation-like set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty set
{0} is non empty trivial functional finite V36() 1 -element empty-membered with_common_domain countable Element of K10(NAT)
0 * is non empty functional V36() FinSequence-membered FinSequenceSet of 0
{0} is non empty trivial functional finite V36() 1 -element empty-membered with_common_domain countable set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
NAT \ {0} is non empty non trivial non finite with_non-empty_elements Element of K10(REAL)
NAT typed\ {0} is countable Element of K10(NAT)
NAT \ {0} is non empty non trivial non finite with_non-empty_elements countable denumerable Element of K10(NAT)
the of S " (NAT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
INT \ NAT is Element of K10(INT)
K10(INT) is non empty non trivial non finite set
INT typed\ NAT is Element of K10(INT)
the of S " (INT \ NAT) is Element of K10(( the carrier of S \ { the OneF of S}))
the of S " NAT is Element of K10(( the carrier of S \ { the OneF of S}))
INT \ {0} is non empty non trivial non finite with_non-empty_elements Element of K10(INT)
INT typed\ {0} is Element of K10(INT)
the of S " (INT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
the ZeroF of S is Element of the carrier of S
{ the ZeroF of S, the OneF of S} is non empty finite countable set
the carrier of S \ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
the carrier of S typed\ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
S is ()
(S) is set
the carrier of S is set
(S) is set
the OneF of S is Element of the carrier of S
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
(S) is set
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is Relation-like set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
1 -tuples_on (S) is functional V36() FinSequence-membered FinSequenceSet of (S)
S is ()
(S) is set
the carrier of S is set
S is ZeroOneStr
the carrier of S is set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
X is Element of the carrier of S \ { the OneF of S}
the ZeroF of S is Element of the carrier of S
- 2 is non empty complex ext-real non positive negative real integer set
S is ZeroOneStr
the carrier of S is set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
X is Element of the carrier of S \ { the OneF of S}
(S,X) is complex ext-real real integer set
S is non empty non degenerated non trivial ZeroOneStr
the carrier of S is non empty non trivial set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
S1 is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
SS1 is Element of the carrier of S \ { the OneF of S}
S1 . SS1 is complex ext-real real integer Element of INT
(S,SS1) is complex ext-real real integer Element of INT
S1 is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
SS1 is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
dom S1 is non empty Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
dom SS1 is non empty Element of K10(( the carrier of S \ { the OneF of S}))
SX is set
add is Element of the carrier of S \ { the OneF of S}
S1 . add is complex ext-real real integer Element of INT
(S,add) is complex ext-real real integer Element of INT
SS1 . add is complex ext-real real integer Element of INT
S1 . SX is set
SS1 . SX is set
the non empty non trivial non finite set is non empty non trivial non finite set
the Element of the non empty non trivial non finite set is Element of the non empty non trivial non finite set
{ the Element of the non empty non trivial non finite set } is non empty trivial finite 1 -element countable Element of K10( the non empty non trivial non finite set )
K10( the non empty non trivial non finite set ) is non empty non trivial non finite set
the non empty non trivial non finite set \ { the Element of the non empty non trivial non finite set } is non empty non trivial non finite Element of K10( the non empty non trivial non finite set )
the non empty non trivial non finite set typed\ { the Element of the non empty non trivial non finite set } is Element of K10( the non empty non trivial non finite set )
the Element of the non empty non trivial non finite set \ { the Element of the non empty non trivial non finite set } is Element of the non empty non trivial non finite set \ { the Element of the non empty non trivial non finite set }
SX is Element of the non empty non trivial non finite set
ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #) is strict ZeroOneStr
1. ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #) is Element of the carrier of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #)
the carrier of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #) is set
the OneF of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #) is Element of the carrier of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #)
0. ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #) is zero Element of the carrier of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #)
the ZeroF of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #) is Element of the carrier of ZeroOneStr(# the non empty non trivial non finite set , the Element of the non empty non trivial non finite set ,SX #)
f is non empty non degenerated non trivial ZeroOneStr
S is non empty non degenerated non trivial non finite ZeroOneStr
the carrier of S is non empty non trivial non finite set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
K10( the carrier of S) is non empty non trivial non finite set
the carrier of S \ { the OneF of S} is non empty non trivial non finite Element of K10( the carrier of S)
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
(S) is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
(S) " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty non trivial non finite set
the ZeroF of S is Element of the carrier of S
{ the ZeroF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} is non empty non trivial non finite Element of K10( the carrier of S)
( the carrier of S \ { the OneF of S}) typed\ { the ZeroF of S} is Element of K10(( the carrier of S \ { the OneF of S}))
( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} is non empty non trivial non finite Element of K10(( the carrier of S \ { the OneF of S}))
dom (S) is non empty Element of K10(( the carrier of S \ { the OneF of S}))
S2 is set
SS2 is Element of the carrier of S \ { the OneF of S}
(S,SS2) is complex ext-real real integer Element of INT
(S) . SS2 is complex ext-real real integer Element of INT
S is non empty non degenerated non trivial ZeroOneStr
(S) is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
the carrier of S is non empty non trivial set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the ZeroF of S is Element of the carrier of S
(S) . the ZeroF of S is set
0. S is zero Element of the carrier of S
1. S is non zero Element of the carrier of S
SX is Element of the carrier of S \ { the OneF of S}
(S) . SX is complex ext-real real integer Element of INT
(S,SX) is complex ext-real real integer Element of INT
the non empty non degenerated non trivial non finite ZeroOneStr is non empty non degenerated non trivial non finite ZeroOneStr
0. the non empty non degenerated non trivial non finite ZeroOneStr is zero Element of the carrier of the non empty non degenerated non trivial non finite ZeroOneStr
the carrier of the non empty non degenerated non trivial non finite ZeroOneStr is non empty non trivial non finite set
the ZeroF of the non empty non degenerated non trivial non finite ZeroOneStr is Element of the carrier of the non empty non degenerated non trivial non finite ZeroOneStr
1. the non empty non degenerated non trivial non finite ZeroOneStr is non zero Element of the carrier of the non empty non degenerated non trivial non finite ZeroOneStr
the OneF of the non empty non degenerated non trivial non finite ZeroOneStr is Element of the carrier of the non empty non degenerated non trivial non finite ZeroOneStr
( the non empty non degenerated non trivial non finite ZeroOneStr ) is non empty Relation-like the carrier of the non empty non degenerated non trivial non finite ZeroOneStr \ { the OneF of the non empty non degenerated non trivial non finite ZeroOneStr } -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr \ { the OneF of the non empty non degenerated non trivial non finite ZeroOneStr }),INT))
{ the OneF of the non empty non degenerated non trivial non finite ZeroOneStr } is non empty trivial finite 1 -element countable Element of K10( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr )
K10( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr ) is non empty non trivial non finite set
the carrier of the non empty non degenerated non trivial non finite ZeroOneStr \ { the OneF of the non empty non degenerated non trivial non finite ZeroOneStr } is non empty non trivial non finite Element of K10( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr )
the carrier of the non empty non degenerated non trivial non finite ZeroOneStr typed\ { the OneF of the non empty non degenerated non trivial non finite ZeroOneStr } is Element of K10( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr )
K11(( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr \ { the OneF of the non empty non degenerated non trivial non finite ZeroOneStr }),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr \ { the OneF of the non empty non degenerated non trivial non finite ZeroOneStr }),INT)) is non empty non trivial non finite set
( the carrier of the non empty non degenerated non trivial non finite ZeroOneStr , the ZeroF of the non empty non degenerated non trivial non finite ZeroOneStr , the OneF of the non empty non degenerated non trivial non finite ZeroOneStr ,( the non empty non degenerated non trivial non finite ZeroOneStr )) is () ()
S1 is () ()
0. S1 is zero Element of the carrier of S1
the carrier of S1 is set
the ZeroF of S1 is Element of the carrier of S1
1. S1 is Element of the carrier of S1
the OneF of S1 is Element of the carrier of S1
the of S1 is Relation-like the carrier of S1 \ { the OneF of S1} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S1 \ { the OneF of S1}),INT))
{ the OneF of S1} is non empty trivial finite 1 -element countable set
the carrier of S1 \ { the OneF of S1} is Element of K10( the carrier of S1)
K10( the carrier of S1) is non empty set
the carrier of S1 typed\ { the OneF of S1} is Element of K10( the carrier of S1)
K11(( the carrier of S1 \ { the OneF of S1}),INT) is Relation-like set
K10(K11(( the carrier of S1 \ { the OneF of S1}),INT)) is non empty set
(S1) is set
the of S1 " {0} is Element of K10(( the carrier of S1 \ { the OneF of S1}))
K10(( the carrier of S1 \ { the OneF of S1})) is non empty set
(S1) is set
the of S1 . (S1) is set
S is ()
S is ()
S is non empty ()
(S) is set
the carrier of S is non empty set
S is () ()
(S) is set
the carrier of S is set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is Relation-like set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
S is non empty non degenerated non trivial () ()
(S) is non empty non trivial non finite set
the carrier of S is non empty non trivial set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
(S) is non empty set
K10((S)) is non empty set
S is non empty non degenerated non trivial ()
(S) is set
the ZeroF of S is Element of the carrier of S
the carrier of S is non empty non trivial set
(S) is non empty set
(S) is set
the OneF of S is Element of the carrier of S
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
1. S is non zero Element of the carrier of S
0. S is zero Element of the carrier of S
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
(S) is set
the ZeroF of S is Element of the carrier of S
(S) is set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " (INT \ NAT) is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
(S) is non empty set
(S) is set
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
dom the of S is non empty Element of K10(( the carrier of S \ { the OneF of S}))
the of S . (S) is set
add is Element of (S)
S is non empty non degenerated non trivial ()
(S) is set
(S) is set
the carrier of S is non empty non trivial set
(S) is set
the OneF of S is Element of the carrier of S
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
S is non empty non degenerated non trivial ()
(S) is set
the ZeroF of S is Element of the carrier of S
the carrier of S is non empty non trivial set
(S) is non empty set
(S) is non empty Element of K10((S))
K10((S)) is non empty set
(S) is set
(S) is set
the OneF of S is Element of the carrier of S
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) is non empty non trivial non finite Element of K10((S))
K10((S)) is non empty set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
(S) is set
the of S " (NAT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) /\ (S) is Element of K10((S))
(S) typed/\ (S) is Element of K10((S))
K10((S)) is non empty non trivial non finite set
(S) /\ (S) is set
(S) /\typed (S) is Element of K10((S))
K10((S)) is non empty set
(S) is set
the of S " NAT is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " (INT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) /\ (S) is set
(S) typed/\ (S) is Element of K10((S))
K10((S)) is non empty set
(S) /\typed (S) is Element of K10((S))
K10((S)) is non empty set
(S) is set
the of S " (INT \ NAT) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the ZeroF of S is Element of the carrier of S
{ the ZeroF of S, the OneF of S} is non empty finite countable set
the carrier of S \ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
the carrier of S typed\ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
(S) \ (S) is Element of K10((S))
K10((S)) is non empty set
(S) typed\ (S) is Element of K10((S))
(S) is non empty Element of K10((S))
(S) is set
(S) is set
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
(S) is Element of (S)
{(S)} is non empty trivial finite 1 -element countable Element of K10((S))
K10((S)) is non empty set
{ the OneF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
{0} /\ (NAT \ {0}) is finite countable Element of K10(REAL)
{0} typed/\ (NAT \ {0}) is trivial functional finite V36() empty-membered with_common_domain countable Element of K10({0})
K10({0}) is non empty finite V36() countable set
{0} /\ (NAT \ {0}) is finite countable set
{0} /\typed (NAT \ {0}) is with_non-empty_elements Element of K10((NAT \ {0}))
K10((NAT \ {0})) is non empty non trivial non finite set
the of S " ({0} /\ (NAT \ {0})) is Element of K10(( the carrier of S \ { the OneF of S}))
the of S " {} is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support Element of K10(( the carrier of S \ { the OneF of S}))
NAT /\ (INT \ {0}) is Element of K10(INT)
NAT typed/\ (INT \ {0}) is countable Element of K10(NAT)
NAT /\ (INT \ {0}) is set
NAT /\typed (INT \ {0}) is with_non-empty_elements Element of K10((INT \ {0}))
K10((INT \ {0})) is non empty non trivial non finite set
the of S " (NAT /\ (INT \ {0})) is Element of K10(( the carrier of S \ { the OneF of S}))
NAT /\ INT is Element of K10(REAL)
NAT typed/\ INT is countable Element of K10(NAT)
NAT /\ INT is set
NAT /\typed INT is Element of K10(INT)
(NAT /\ INT) \ {0} is with_non-empty_elements Element of K10(REAL)
(NAT /\ INT) typed\ {0} is Element of K10((NAT /\ INT))
K10((NAT /\ INT)) is non empty set
(NAT /\ INT) \ {0} is with_non-empty_elements Element of K10((NAT /\ INT))
the of S " ((NAT /\ INT) \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
{ the ZeroF of S} is non empty trivial finite 1 -element countable Element of K10( the carrier of S)
{ the ZeroF of S} \/ { the OneF of S} is non empty finite countable Element of K10( the carrier of S)
(S) \ ({ the ZeroF of S} \/ { the OneF of S}) is Element of K10((S))
(S) typed\ ({ the ZeroF of S} \/ { the OneF of S}) is Element of K10((S))
( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} is Element of K10( the carrier of S)
( the carrier of S \ { the OneF of S}) typed\ { the ZeroF of S} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} is Element of K10(( the carrier of S \ { the OneF of S}))
(S) \ ( the carrier of S \ { the OneF of S}) is Element of K10((S))
(S) typed\ ( the carrier of S \ { the OneF of S}) is Element of K10((S))
(S) /\ { the ZeroF of S} is finite countable Element of K10( the carrier of S)
(S) typed/\ { the ZeroF of S} is Element of K10((S))
(S) /\ { the ZeroF of S} is finite countable set
(S) /\typed { the ZeroF of S} is trivial finite countable Element of K10({ the ZeroF of S})
K10({ the ZeroF of S}) is non empty finite V36() countable set
((S) \ ( the carrier of S \ { the OneF of S})) \/ ((S) /\ { the ZeroF of S}) is set
{} \/ ((S) /\ { the ZeroF of S}) is finite countable set
the of S " INT is Element of K10(( the carrier of S \ { the OneF of S}))
( the of S " INT) \ ( the of S " NAT) is Element of K10(( the carrier of S \ { the OneF of S}))
( the of S " INT) typed\ ( the of S " NAT) is Element of K10(( the of S " INT))
K10(( the of S " INT)) is non empty set
( the of S " INT) \ ( the of S " NAT) is Element of K10(( the of S " INT))
( the of S " INT) \ ( the of S " {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
( the of S " INT) typed\ ( the of S " {0}) is Element of K10(( the of S " INT))
( the of S " INT) \ ( the of S " {0}) is Element of K10(( the of S " INT))
( the of S " NAT) \ ( the of S " {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
( the of S " NAT) typed\ ( the of S " {0}) is Element of K10(( the of S " NAT))
K10(( the of S " NAT)) is non empty set
( the of S " NAT) \ ( the of S " {0}) is Element of K10(( the of S " NAT))
the of S . (S) is set
the of S . the ZeroF of S is set
{ the OneF of S} \/ { the ZeroF of S} is non empty finite countable Element of K10( the carrier of S)
the carrier of S \ ({ the OneF of S} \/ { the ZeroF of S}) is Element of K10( the carrier of S)
the carrier of S typed\ ({ the OneF of S} \/ { the ZeroF of S}) is Element of K10( the carrier of S)
NN2 is set
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " NAT is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
(S) is non empty non trivial non finite Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
X is set
(S) is set
X is Element of (S)
(S) is set
the ZeroF of S is Element of the carrier of S
{ the ZeroF of S, the OneF of S} is non empty finite countable set
the carrier of S \ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
the carrier of S typed\ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
(S) is non empty Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
(S) is set
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
X is Element of (S)
(S) is set
the of S " (INT \ NAT) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " (INT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
X is Element of (S)
(S) is set
the of S " (NAT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
X is Element of (S)
(S) is non empty non trivial non finite Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
X is Element of (S)
(S) is set
the ZeroF of S is Element of the carrier of S
{ the ZeroF of S, the OneF of S} is non empty finite countable set
the carrier of S \ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
the carrier of S typed\ { the ZeroF of S, the OneF of S} is Element of K10( the carrier of S)
X is Element of (S)
(S) is set
the of S " (NAT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " (INT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
X is Element of (S)
(S) is set
the of S " (INT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is non empty Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
(S) is set
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
(S) is set
the of S " (INT \ NAT) is Element of K10(( the carrier of S \ { the OneF of S}))
(S) /\ (S) is set
(S) typed/\ (S) is Element of K10((S))
K10((S)) is non empty set
(S) /\typed (S) is Element of K10((S))
K10((S)) is non empty set
NAT /\ (INT \ NAT) is Element of K10(INT)
NAT typed/\ (INT \ NAT) is countable Element of K10(NAT)
NAT /\ (INT \ NAT) is set
NAT /\typed (INT \ NAT) is Element of K10((INT \ NAT))
K10((INT \ NAT)) is non empty set
the of S " (NAT /\ (INT \ NAT)) is Element of K10(( the carrier of S \ { the OneF of S}))
NAT /\ INT is Element of K10(REAL)
NAT typed/\ INT is countable Element of K10(NAT)
NAT /\ INT is set
NAT /\typed INT is Element of K10(INT)
NAT /\ NAT is Element of K10(REAL)
NAT typed/\ NAT is countable Element of K10(NAT)
NAT /\ NAT is set
NAT /\typed NAT is countable Element of K10(NAT)
(NAT /\ INT) \ (NAT /\ NAT) is Element of K10(REAL)
(NAT /\ INT) typed\ (NAT /\ NAT) is Element of K10((NAT /\ INT))
K10((NAT /\ INT)) is non empty set
(NAT /\ INT) \ (NAT /\ NAT) is Element of K10((NAT /\ INT))
the of S " ((NAT /\ INT) \ (NAT /\ NAT)) is Element of K10(( the carrier of S \ { the OneF of S}))
the of S " {} is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element real integer FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V160() empty-membered Cardinal-yielding countable FinSequence-yielding finite-support Element of K10(( the carrier of S \ { the OneF of S}))
(S) \ (S) is Element of K10((S))
(S) typed\ (S) is Element of K10((S))
SX is Element of (S)
X is Element of (S)
(S) is non empty non trivial non finite Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " (NAT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
SS1 is Element of (S)
(S) /\ (S) is Element of K10((S))
(S) typed/\ (S) is Element of K10((S))
K10((S)) is non empty non trivial non finite set
(S) /\ (S) is set
(S) /\typed (S) is Element of K10((S))
K10((S)) is non empty set
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
(S) is non empty set
(S) is non empty Element of K10((S))
K10((S)) is non empty set
(S) is set
the OneF of S is Element of the carrier of S
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
(S) is Element of (S)
the ZeroF of S is Element of the carrier of S
X is Element of (S)
(S) is non empty set
(S) is non empty non trivial non finite Element of K10((S))
K10((S)) is non empty set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
the Element of (S) is Element of (S)
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
(S) is set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " (INT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
(S) is non empty set
the of S " NAT is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " (NAT \ {0}) is Element of K10(( the carrier of S \ { the OneF of S}))
SX is (S) (S) Element of (S)
(S) /\ (S) is set
(S) typed/\ (S) is Element of K10((S))
K10((S)) is non empty set
(S) /\typed (S) is Element of K10((S))
K10((S)) is non empty set
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
the (S) (S) (S) (S) (S) (S) Element of (S) is (S) (S) (S) (S) (S) (S) Element of (S)
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
X is (S) Element of (S)
the of S . X is set
(S) is non empty Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
(S) is set
{(S)} is non empty trivial finite 1 -element countable set
(S) \ {(S)} is Element of K10((S))
K10((S)) is non empty set
(S) typed\ {(S)} is Element of K10((S))
K11((S),INT) is non empty non trivial Relation-like non finite set
K10(K11((S),INT)) is non empty non trivial non finite set
SS1 is non empty Relation-like (S) -defined INT -valued Function-like total quasi_total Element of K10(K11((S),INT))
SX is Element of (S)
SS1 . SX is complex ext-real real integer Element of INT
S is non empty non degenerated non trivial () ()
(S) is set
the carrier of S is non empty non trivial set
X is (S) (S) (S) (S) (S) (S) Element of (S)
(S,X) is complex ext-real real integer Element of INT
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S . X is set
(S) is non empty non trivial non finite Element of K10((S))
(S) is non empty set
K10((S)) is non empty set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
SS1 is set
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) -concatenation is non empty Relation-like K11(((S) *),((S) *)) -defined (S) * -valued Function-like total quasi_total associative Function-yielding V160() FinSequence-yielding Element of K10(K11(K11(((S) *),((S) *)),((S) *)))
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
K11(((S) *),((S) *)) is non empty non trivial Relation-like non finite set
K11(K11(((S) *),((S) *)),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(K11(((S) *),((S) *)),((S) *))) is non empty non trivial non finite set
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) -multiCat is non empty Relation-like ((S) *) * -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11((((S) *) *),((S) *)))
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
((S) *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S) *
K11((((S) *) *),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11((((S) *) *),((S) *))) is non empty non trivial non finite set
{} .--> {} is trivial Relation-like {{}} -defined Function-like one-to-one constant finite Function-yielding V160() Cardinal-yielding countable finite-support set
{{}} --> {} is non empty Relation-like empty-yielding {{}} -defined {{}} -valued Function-like constant total quasi_total finite Function-yielding V160() Cardinal-yielding countable finite-support Element of K10(K11({{}},{{}}))
K11({{}},{{}}) is non empty Relation-like finite countable set
K10(K11({{}},{{}})) is non empty finite V36() countable set
(S) -concatenation is non empty Relation-like K11(((S) *),((S) *)) -defined (S) * -valued Function-like total quasi_total associative Function-yielding V160() FinSequence-yielding Element of K10(K11(K11(((S) *),((S) *)),((S) *)))
K11(((S) *),((S) *)) is non empty non trivial Relation-like non finite set
K11(K11(((S) *),((S) *)),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(K11(((S) *),((S) *)),((S) *))) is non empty non trivial non finite set
MultPlace ((S) -concatenation) is non empty Relation-like (((S) *) *) \ {{}} -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11(((((S) *) *) \ {{}}),((S) *)))
(((S) *) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10((((S) *) *))
K10((((S) *) *)) is non empty non trivial non finite set
(((S) *) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10((((S) *) *))
K11(((((S) *) *) \ {{}}),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(((((S) *) *) \ {{}}),((S) *))) is non empty non trivial non finite set
({} .--> {}) +* (MultPlace ((S) -concatenation)) is non empty Relation-like Function-like Function-yielding V160() set
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) -firstChar is non empty Relation-like ((S) *) \ {{}} -defined (S) -valued Function-like total quasi_total Element of K10(K11((((S) *) \ {{}}),(S)))
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
((S) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10(((S) *))
K10(((S) *)) is non empty non trivial non finite set
((S) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10(((S) *))
K11((((S) *) \ {{}}),(S)) is non empty non trivial Relation-like non finite set
K10(K11((((S) *) \ {{}}),(S))) is non empty non trivial non finite set
(S) -pr1 is non empty Relation-like K11((S),(S)) -defined (S) -valued Function-like total quasi_total associative Element of K10(K11(K11((S),(S)),(S)))
K11((S),(S)) is non empty Relation-like set
K11(K11((S),(S)),(S)) is non empty Relation-like set
K10(K11(K11((S),(S)),(S))) is non empty set
K530((S),(S)) is non empty Relation-like K11((S),(S)) -defined (S) -valued Function-like total quasi_total Element of K10(K11(K11((S),(S)),(S)))
MultPlace ((S) -pr1) is non empty Relation-like ((S) *) \ {{}} -defined (S) -valued Function-like total quasi_total Element of K10(K11((((S) *) \ {{}}),(S)))
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
X is set
X is set
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
((S) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10(((S) *))
K10(((S) *)) is non empty non trivial non finite set
((S) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10(((S) *))
X is set
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
((S) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10(((S) *))
K10(((S) *)) is non empty non trivial non finite set
((S) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10(((S) *))
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of ((S) *) \ {{}}
S is non empty non degenerated non trivial () ()
(S) is non empty set
the carrier of S is non empty non trivial set
(S) is non empty non trivial non finite Element of K10((S))
K10((S)) is non empty set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty set
(S) \/ (S) is non empty non trivial non finite set
S is non empty non degenerated non trivial non finite () ()
(S) is non empty set
the carrier of S is non empty non trivial non finite set
S is non empty non degenerated non trivial non finite () ()
(S) is non empty non trivial non finite set
the carrier of S is non empty non trivial non finite set
(S) is non empty non trivial non finite set
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
((S) *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S) *
X is (S) Element of (S)
<*X*> is non empty trivial Relation-like NAT -defined (S) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of 1 -tuples_on (S)
1 -tuples_on (S) is non empty functional V36() FinSequence-membered with_non-empty_elements FinSequenceSet of (S)
(S) is non empty Relation-like ((S) *) * -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11((((S) *) *),((S) *)))
K11((((S) *) *),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11((((S) *) *),((S) *))) is non empty non trivial non finite set
(S) -multiCat is non empty Relation-like ((S) *) * -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11((((S) *) *),((S) *)))
(S) -concatenation is non empty Relation-like K11(((S) *),((S) *)) -defined (S) * -valued Function-like total quasi_total associative Function-yielding V160() FinSequence-yielding Element of K10(K11(K11(((S) *),((S) *)),((S) *)))
K11(((S) *),((S) *)) is non empty non trivial Relation-like non finite set
K11(K11(((S) *),((S) *)),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(K11(((S) *),((S) *)),((S) *))) is non empty non trivial non finite set
MultPlace ((S) -concatenation) is non empty Relation-like (((S) *) *) \ {{}} -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11(((((S) *) *) \ {{}}),((S) *)))
(((S) *) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10((((S) *) *))
K10((((S) *) *)) is non empty non trivial non finite set
(((S) *) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10((((S) *) *))
K11(((((S) *) *) \ {{}}),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(((((S) *) *) \ {{}}),((S) *))) is non empty non trivial non finite set
({} .--> {}) +* (MultPlace ((S) -concatenation)) is non empty Relation-like Function-like Function-yielding V160() set
S1 is set
(S,X) is complex ext-real real integer Element of INT
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty non trivial non finite Element of K10( the carrier of S)
K10( the carrier of S) is non empty non trivial non finite set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S . X is set
abs (S,X) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative finite cardinal real integer countable Element of NAT
{ (<*X*> ^ ((S) . b1)) where b1 is Relation-like NAT -defined (S) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V160() countable FinSequence-yielding finite-support Element of ((S) *) * : ( rng b1 c= S1 & b1 is abs (S,X) -element ) } is set
S is non empty non degenerated non trivial non finite () ()
(S) is non empty non trivial non finite set
the carrier of S is non empty non trivial non finite set
X is (S) Element of (S)
S1 is set
(S,X,S1) is set
(S) is non empty non trivial non finite set
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
((S) *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S) *
<*X*> is non empty trivial Relation-like NAT -defined (S) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of 1 -tuples_on (S)
1 -tuples_on (S) is non empty functional V36() FinSequence-membered with_non-empty_elements FinSequenceSet of (S)
(S) is non empty Relation-like ((S) *) * -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11((((S) *) *),((S) *)))
K11((((S) *) *),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11((((S) *) *),((S) *))) is non empty non trivial non finite set
(S) -multiCat is non empty Relation-like ((S) *) * -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11((((S) *) *),((S) *)))
(S) -concatenation is non empty Relation-like K11(((S) *),((S) *)) -defined (S) * -valued Function-like total quasi_total associative Function-yielding V160() FinSequence-yielding Element of K10(K11(K11(((S) *),((S) *)),((S) *)))
K11(((S) *),((S) *)) is non empty non trivial Relation-like non finite set
K11(K11(((S) *),((S) *)),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(K11(((S) *),((S) *)),((S) *))) is non empty non trivial non finite set
MultPlace ((S) -concatenation) is non empty Relation-like (((S) *) *) \ {{}} -defined (S) * -valued Function-like total quasi_total Function-yielding V160() FinSequence-yielding Element of K10(K11(((((S) *) *) \ {{}}),((S) *)))
(((S) *) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10((((S) *) *))
K10((((S) *) *)) is non empty non trivial non finite set
(((S) *) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10((((S) *) *))
K11(((((S) *) *) \ {{}}),((S) *)) is non empty non trivial Relation-like non finite set
K10(K11(((((S) *) *) \ {{}}),((S) *))) is non empty non trivial non finite set
({} .--> {}) +* (MultPlace ((S) -concatenation)) is non empty Relation-like Function-like Function-yielding V160() set
(S,X) is complex ext-real real integer Element of INT
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty non trivial non finite Element of K10( the carrier of S)
K10( the carrier of S) is non empty non trivial non finite set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S . X is set
abs (S,X) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative finite cardinal real integer countable Element of NAT
{ (<*X*> ^ ((S) . b1)) where b1 is Relation-like NAT -defined (S) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V160() countable FinSequence-yielding finite-support Element of ((S) *) * : ( rng b1 c= S1 & b1 is abs (S,X) -element ) } is set
((S) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements Element of K10(((S) *))
K10(((S) *)) is non empty non trivial non finite set
((S) *) typed\ {{}} is functional V36() FinSequence-membered Element of K10(((S) *))
K10((((S) *) \ {{}})) is non empty non trivial non finite set
bool (((S) *) \ {{}}) is non empty non trivial non finite Element of K10(K10((((S) *) \ {{}})))
K10(K10((((S) *) \ {{}}))) is non empty non trivial non finite set
f is set
S2 is Relation-like NAT -defined (S) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V160() countable FinSequence-yielding finite-support Element of ((S) *) *
(S) . S2 is Relation-like NAT -defined (S) -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (S) *
<*X*> ^ ((S) . S2) is non empty Relation-like NAT -defined (S) -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
rng S2 is functional finite V36() FinSequence-membered countable Element of K10(((S) *))
add is Element of (S)
<*add*> is non empty trivial Relation-like NAT -defined (S) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of 1 -tuples_on (S)
1 -tuples_on (S) is non empty functional V36() FinSequence-membered with_non-empty_elements FinSequenceSet of (S)
SS2 is non empty Relation-like NAT -defined (S) -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of (S)
E1 is Relation-like NAT -defined (S) -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of (S)
SS2 ^ E1 is non empty Relation-like NAT -defined (S) -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (S) *
S is non empty non degenerated non trivial non finite () ()
(S) is set
(S) is non empty non trivial non finite set
the carrier of S is non empty non trivial non finite set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty non trivial non finite Element of K10( the carrier of S)
K10( the carrier of S) is non empty non trivial non finite set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty non trivial non finite set
1 -tuples_on (S) is non empty functional V36() FinSequence-membered with_non-empty_elements FinSequenceSet of (S)
(S) is non empty non trivial non finite set
{ (S,b1,a2) where b1 is (S) Element of (S) : b1 is (S) } is set
union { (S,b1,a2) where b1 is (S) Element of (S) : b1 is (S) } is set
X is Relation-like Function-like set
dom X is set
X . 0 is set
{ (S,b1,a2) where b1 is (S) Element of (S) : b1 is (S) } is set
union { (S,b1,a2) where b1 is (S) Element of (S) : b1 is (S) } is set
X is Relation-like Function-like set
dom X is set
X . 0 is set
S1 is Relation-like Function-like set
dom S1 is set
S1 . 0 is set
SS1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative finite cardinal real integer countable set
SS1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative finite cardinal real integer countable set
X . (SS1 + 1) is set
X . SS1 is set
{ (S,b1,(X . SS1)) where b1 is (S) Element of (S) : b1 is (S) } is set
union { (S,b1,(X . SS1)) where b1 is (S) Element of (S) : b1 is (S) } is set
(union { (S,b1,(X . SS1)) where b1 is (S) Element of (S) : b1 is (S) } ) \/ (X . SS1) is set
SS1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative finite cardinal real integer countable set
SS1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative finite cardinal real integer countable set
S1 . (SS1 + 1) is set
S1 . SS1 is set
{ (S,b1,(S1 . SS1)) where b1 is (S) Element of (S) : b1 is (S) } is set
union { (S,b1,(S1 . SS1)) where b1 is (S) Element of (S) : b1 is (S) } is set
(union { (S,b1,(S1 . SS1)) where b1 is (S) Element of (S) : b1 is (S) } ) \/ (S1 . SS1) is set
S is non empty non degenerated non trivial non finite () ()
(S) is set
(S) is non empty non trivial non finite set
the carrier of S is non empty non trivial non finite set
the OneF of S is Element of the carrier of S
{ the OneF of S} is non empty trivial finite 1 -element countable set
the carrier of S \ { the OneF of S} is non empty non trivial non finite Element of K10( the carrier of S)
K10( the carrier of S) is non empty non trivial non finite set
the carrier of S typed\ { the OneF of S} is Element of K10( the carrier of S)
the of S is non empty Relation-like the carrier of S \ { the OneF of S} -defined INT -valued Function-like total quasi_total Element of K10(K11(( the carrier of S \ { the OneF of S}),INT))
K11(( the carrier of S \ { the OneF of S}),INT) is non empty non trivial Relation-like non finite set
K10(K11(( the carrier of S \ { the OneF of S}),INT)) is non empty non trivial non finite set
the of S " {0} is Element of K10(( the carrier of S \ { the OneF of S}))
K10(( the carrier of S \ { the OneF of S})) is non empty non trivial non finite set
1 -tuples_on (S) is non empty functional V36() FinSequence-membered with_non-empty_elements FinSequenceSet of (S)
(S) is non empty non trivial non finite set
(S) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (S)
K10(((S) *)) is non empty non trivial non finite set
K10((S)) is non empty non tri