:: FOMODEL1 semantic presentation

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

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

((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,b

union { (S,b

X is Relation-like Function-like set

dom X is set

X . 0 is set

{ (S,b

union { (S,b

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,b

union { (S,b

(union { (S,b

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,b

union { (S,b

(union { (S,b

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