:: FOMODEL1 semantic presentation

REAL is non empty non trivial non finite set

K10(REAL) is non empty non trivial non finite 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

K11(,NAT) is non empty non trivial Relation-like non finite set
is 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

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

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

- 1 is non empty complex ext-real non positive negative 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

the 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
NAT \ is non empty non trivial non finite with_non-empty_elements Element of K10(REAL)

the of S " () 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

the of S " () 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 \ is non empty non trivial non finite with_non-empty_elements Element of K10(INT)

the of S " () 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 " 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}

(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}

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

K10() is non empty finite V36() countable set

K10(()) is non empty non trivial non finite set
the of S " ( /\ ()) is Element of K10(( the carrier of S \ { the OneF of S}))

NAT /\ () is Element of K10(INT)
NAT typed/\ () is countable Element of K10(NAT)
NAT /\ () is set

K10(()) is non empty non trivial non finite set
the of S " (NAT /\ ()) is Element of K10(( the carrier of S \ { the OneF of S}))
NAT /\ INT is Element of K10(REAL)

() typed\ is Element of K10(())
K10(()) is non empty set
() \ is with_non-empty_elements Element of K10(())
the of S " (() \ ) 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 " ) is Element of K10(( the carrier of S \ { the OneF of S}))
( the of S " INT) typed\ ( the of S " ) is Element of K10(( the of S " INT))
( the of S " INT) \ ( the of S " ) is Element of K10(( the of S " INT))
( the of S " NAT) \ ( the of S " ) is Element of K10(( the carrier of S \ { the OneF of S}))
( the of S " NAT) typed\ ( the of S " ) is Element of K10(( the of S " NAT))
K10(( the of S " NAT)) is non empty set
( the of S " NAT) \ ( the of S " ) 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 " 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 " () is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " () is Element of K10(( the carrier of S \ { the OneF of S}))
X is Element of (S)
(S) is set
the of S " () 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 " 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 " () is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " () is Element of K10(( the carrier of S \ { the OneF of S}))
X is Element of (S)
(S) is set
the of S " () 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 " () 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 /\ () is Element of K10(INT)
NAT typed/\ () is countable Element of K10(NAT)
NAT /\ () is set
NAT /\typed () is Element of K10(())
K10(()) is non empty set
the of S " (NAT /\ ()) is Element of K10(( the carrier of S \ { the OneF of S}))
NAT /\ INT is Element of K10(REAL)

NAT /\ NAT is Element of K10(REAL)

() \ () is Element of K10(REAL)
() typed\ () is Element of K10(())
K10(()) is non empty set
() \ () is Element of K10(())
the of S " (() \ ()) 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))
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 " is Element of K10(( the carrier of S \ { the OneF of S}))
(S) is set
the of S " () 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 " 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 " () 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 " () 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)

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

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

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

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

{ (<*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) *

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

{ (<*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

rng S2 is functional finite V36() FinSequence-membered countable Element of K10(((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 " 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

(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

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

dom X is set
X . 0 is set

dom S1 is set
S1 . 0 is 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

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

(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