:: CSSPACE semantic presentation

REAL is non empty V52() V64() V65() V66() V70() set
NAT is non empty V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V52() V64() V70() set
NAT is non empty V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() set
bool NAT is non empty set
bool NAT is non empty set
RAT is non empty V52() V64() V65() V66() V67() V70() set
INT is non empty V52() V64() V65() V66() V67() V68() V70() set
[:NAT,REAL:] is non empty V38() V39() V40() set
bool [:NAT,REAL:] is non empty set
[:NAT,COMPLEX:] is non empty V38() set
bool [:NAT,COMPLEX:] is non empty set
{} is Function-like functional empty V26() V27() V28() V30() V31() V32() complex ext-real non positive non negative V64() V65() V66() V67() V68() V69() V70() set
1 is non empty V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
0 is Function-like functional empty V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() Element of NAT
sqrt 0 is complex V34() ext-real Element of REAL
1r is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
Re 0 is complex V34() ext-real Element of REAL
Im 0 is complex V34() ext-real Element of REAL
<i> is complex Element of COMPLEX
0 *' is complex Element of COMPLEX
1r *' is complex Element of COMPLEX
|.0.| is complex V34() ext-real V63() Element of REAL
|.1r.| is complex V34() ext-real Element of REAL
Funcs (NAT,COMPLEX) is functional non empty FUNCTION_DOMAIN of NAT , COMPLEX
V0 is set
the Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:] is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
nilfunc is non empty set
X0 is set
X0 is set
seq is set
V0 is non empty set
nilfunc is non empty set
X0 is set
X0 is set
() is non empty set
V0 is set
V0 is set
[:(),():] is non empty set
[:[:(),():],():] is non empty set
bool [:[:(),():],():] is non empty set
V0 is Element of ()
nilfunc is Element of ()
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Relation-like [:(),():] -defined () -valued Function-like non empty V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
V0 is Relation-like [:(),():] -defined () -valued Function-like non empty V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
V0 is Relation-like [:(),():] -defined () -valued Function-like non empty V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
nilfunc is Relation-like [:(),():] -defined () -valued Function-like non empty V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
() is Relation-like [:(),():] -defined () -valued Function-like non empty V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:COMPLEX,():] is non empty set
[:[:COMPLEX,():],():] is non empty set
bool [:[:COMPLEX,():],():] is non empty set
V0 is set
nilfunc is set
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) is complex set
(V0) (#) (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Relation-like [:COMPLEX,():] -defined () -valued Function-like non empty V14([:COMPLEX,():]) quasi_total Element of bool [:[:COMPLEX,():],():]
nilfunc is set
X0 is set
V0 . (nilfunc,X0) is set
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
V0 . [nilfunc,X0] is set
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) is complex set
(nilfunc) (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Relation-like [:COMPLEX,():] -defined () -valued Function-like non empty V14([:COMPLEX,():]) quasi_total Element of bool [:[:COMPLEX,():],():]
nilfunc is Relation-like [:COMPLEX,():] -defined () -valued Function-like non empty V14([:COMPLEX,():]) quasi_total Element of bool [:[:COMPLEX,():],():]
X0 is complex Element of COMPLEX
seq is Element of ()
V0 . (X0,seq) is Element of ()
[X0,seq] is set
{X0,seq} is non empty set
{X0} is non empty V64() set
{{X0,seq},{X0}} is non empty set
V0 . [X0,seq] is set
nilfunc . (X0,seq) is Element of ()
nilfunc . [X0,seq] is set
(seq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(X0) is complex set
(X0) (#) (seq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
() is Relation-like [:COMPLEX,():] -defined () -valued Function-like non empty V14([:COMPLEX,():]) quasi_total Element of bool [:[:COMPLEX,():],():]
0c is Function-like functional empty V26() V27() V28() V30() V31() V32() complex ext-real non positive non negative V64() V65() V66() V67() V68() V69() V70() Element of COMPLEX
NAT --> 0c is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() V41() Element of bool [:NAT,COMPLEX:]
V0 is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
nilfunc is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
V0 . nilfunc is complex Element of COMPLEX
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Element of ()
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
nilfunc is Element of ()
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
X0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(V0) . X0 is complex Element of COMPLEX
(nilfunc) . X0 is complex Element of COMPLEX
() is Element of ()
V0 is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
CLSStruct(# (),(),(),() #) is non empty strict CLSStruct
the carrier of CLSStruct(# (),(),(),() #) is non empty set
V0 is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
V0 + nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . (V0,nilfunc) is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,nilfunc] is set
{V0,nilfunc} is non empty set
{V0} is non empty set
{{V0,nilfunc},{V0}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [V0,nilfunc] is set
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is complex set
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
V0 * nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
the Mult of CLSStruct(# (),(),(),() #) is Relation-like [:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[V0,nilfunc] is set
{V0,nilfunc} is non empty set
{V0} is non empty V64() set
{{V0,nilfunc},{V0}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [V0,nilfunc] is set
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
() . (V0,nilfunc) is set
() . [V0,nilfunc] is set
(V0) is complex set
(V0) (#) (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
V0 + nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . (V0,nilfunc) is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,nilfunc] is set
{V0,nilfunc} is non empty set
{V0} is non empty set
{{V0,nilfunc},{V0}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [V0,nilfunc] is set
nilfunc + V0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) . (nilfunc,V0) is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,V0] is set
{nilfunc,V0} is non empty set
{nilfunc} is non empty set
{{nilfunc,V0},{nilfunc}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [nilfunc,V0] is set
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
V0 + nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . (V0,nilfunc) is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,nilfunc] is set
{V0,nilfunc} is non empty set
{V0} is non empty set
{{V0,nilfunc},{V0}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [V0,nilfunc] is set
X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
(V0 + nilfunc) + X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) . ((V0 + nilfunc),X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
[(V0 + nilfunc),X0] is set
{(V0 + nilfunc),X0} is non empty set
{(V0 + nilfunc)} is non empty set
{{(V0 + nilfunc),X0},{(V0 + nilfunc)}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [(V0 + nilfunc),X0] is set
nilfunc + X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) . (nilfunc,X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [nilfunc,X0] is set
V0 + (nilfunc + X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) . (V0,(nilfunc + X0)) is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,(nilfunc + X0)] is set
{V0,(nilfunc + X0)} is non empty set
{{V0,(nilfunc + X0)},{V0}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [V0,(nilfunc + X0)] is set
((V0 + nilfunc)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 + nilfunc)) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(((V0) + (nilfunc))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(((V0) + (nilfunc))) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0) + (nilfunc)) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + ((nilfunc) + (X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(((nilfunc) + (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + (((nilfunc) + (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((nilfunc + X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0) + ((nilfunc + X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
0. CLSStruct(# (),(),(),() #) is zero Element of the carrier of CLSStruct(# (),(),(),() #)
the ZeroF of CLSStruct(# (),(),(),() #) is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc + (0. CLSStruct(# (),(),(),() #)) is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . (nilfunc,(0. CLSStruct(# (),(),(),() #))) is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,(0. CLSStruct(# (),(),(),() #))] is set
{nilfunc,(0. CLSStruct(# (),(),(),() #))} is non empty set
{nilfunc} is non empty set
{{nilfunc,(0. CLSStruct(# (),(),(),() #))},{nilfunc}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [nilfunc,(0. CLSStruct(# (),(),(),() #))] is set
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(()) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) + (()) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
X0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
((nilfunc) + (())) . X0 is complex Element of COMPLEX
(nilfunc) . X0 is complex Element of COMPLEX
(()) . X0 is complex Element of COMPLEX
((nilfunc) . X0) + ((()) . X0) is complex Element of COMPLEX
((nilfunc) . X0) + 0c is complex Element of COMPLEX
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
- (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) + (- (nilfunc)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(()) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
seq is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
((nilfunc) + (- (nilfunc))) . seq is complex Element of COMPLEX
(()) . seq is complex Element of COMPLEX
(nilfunc) . seq is complex Element of COMPLEX
(- (nilfunc)) . seq is complex Element of COMPLEX
((nilfunc) . seq) + ((- (nilfunc)) . seq) is complex Element of COMPLEX
- ((nilfunc) . seq) is complex Element of COMPLEX
((nilfunc) . seq) + (- ((nilfunc) . seq)) is complex Element of COMPLEX
X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc + X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . (nilfunc,X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [nilfunc,X0] is set
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is complex set
nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
nilfunc + X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . (nilfunc,X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [nilfunc,X0] is set
V0 * (nilfunc + X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
the Mult of CLSStruct(# (),(),(),() #) is Relation-like [:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[V0,(nilfunc + X0)] is set
{V0,(nilfunc + X0)} is non empty set
{V0} is non empty V64() set
{{V0,(nilfunc + X0)},{V0}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [V0,(nilfunc + X0)] is set
V0 * nilfunc is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,nilfunc] is set
{V0,nilfunc} is non empty set
{{V0,nilfunc},{V0}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [V0,nilfunc] is set
V0 * X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,X0] is set
{V0,X0} is non empty set
{{V0,X0},{V0}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [V0,X0] is set
(V0 * nilfunc) + (V0 * X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) . ((V0 * nilfunc),(V0 * X0)) is Element of the carrier of CLSStruct(# (),(),(),() #)
[(V0 * nilfunc),(V0 * X0)] is set
{(V0 * nilfunc),(V0 * X0)} is non empty set
{(V0 * nilfunc)} is non empty set
{{(V0 * nilfunc),(V0 * X0)},{(V0 * nilfunc)}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [(V0 * nilfunc),(V0 * X0)] is set
((nilfunc + X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) ((nilfunc + X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(nilfunc) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(((nilfunc) + (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) (((nilfunc) + (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) ((nilfunc) + (X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) (nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0 (#) (nilfunc)) + (V0 (#) (X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 * nilfunc)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 * nilfunc)) + ((V0 * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (nilfunc))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (nilfunc))) + ((V0 * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (nilfunc))) + ((V0 (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0 (#) (nilfunc)) + ((V0 (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is complex set
nilfunc is complex set
V0 + nilfunc is complex set
X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
(V0 + nilfunc) * X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the Mult of CLSStruct(# (),(),(),() #) is Relation-like [:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[(V0 + nilfunc),X0] is set
{(V0 + nilfunc),X0} is non empty set
{(V0 + nilfunc)} is non empty V64() set
{{(V0 + nilfunc),X0},{(V0 + nilfunc)}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [(V0 + nilfunc),X0] is set
V0 * X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,X0] is set
{V0,X0} is non empty set
{V0} is non empty V64() set
{{V0,X0},{V0}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [V0,X0] is set
nilfunc * X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty V64() set
{{nilfunc,X0},{nilfunc}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [nilfunc,X0] is set
(V0 * X0) + (nilfunc * X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
the addF of CLSStruct(# (),(),(),() #) is Relation-like [: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[: the carrier of CLSStruct(# (),(),(),() #), the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
the addF of CLSStruct(# (),(),(),() #) . ((V0 * X0),(nilfunc * X0)) is Element of the carrier of CLSStruct(# (),(),(),() #)
[(V0 * X0),(nilfunc * X0)] is set
{(V0 * X0),(nilfunc * X0)} is non empty set
{(V0 * X0)} is non empty set
{{(V0 * X0),(nilfunc * X0)},{(V0 * X0)}} is non empty set
the addF of CLSStruct(# (),(),(),() #) . [(V0 * X0),(nilfunc * X0)] is set
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0 + nilfunc) (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
nilfunc (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0 (#) (X0)) + (nilfunc (#) (X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
seq is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
((V0 + nilfunc) (#) (X0)) . seq is complex Element of COMPLEX
((V0 (#) (X0)) + (nilfunc (#) (X0))) . seq is complex Element of COMPLEX
(X0) . seq is complex Element of COMPLEX
(V0 + nilfunc) * ((X0) . seq) is complex set
V0 * ((X0) . seq) is complex set
nilfunc * ((X0) . seq) is complex set
(V0 * ((X0) . seq)) + (nilfunc * ((X0) . seq)) is complex set
(V0 (#) (X0)) . seq is complex Element of COMPLEX
((V0 (#) (X0)) . seq) + (nilfunc * ((X0) . seq)) is complex set
(nilfunc (#) (X0)) . seq is complex Element of COMPLEX
((V0 (#) (X0)) . seq) + ((nilfunc (#) (X0)) . seq) is complex Element of COMPLEX
((V0 * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((nilfunc * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 * X0)) + ((nilfunc * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (X0))) + ((nilfunc * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((nilfunc (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((V0 (#) (X0))) + ((nilfunc (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0 (#) (X0)) + ((nilfunc (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is complex set
nilfunc is complex set
V0 * nilfunc is complex set
X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
(V0 * nilfunc) * X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the Mult of CLSStruct(# (),(),(),() #) is Relation-like [:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[(V0 * nilfunc),X0] is set
{(V0 * nilfunc),X0} is non empty set
{(V0 * nilfunc)} is non empty V64() set
{{(V0 * nilfunc),X0},{(V0 * nilfunc)}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [(V0 * nilfunc),X0] is set
nilfunc * X0 is Element of the carrier of CLSStruct(# (),(),(),() #)
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty V64() set
{{nilfunc,X0},{nilfunc}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [nilfunc,X0] is set
V0 * (nilfunc * X0) is Element of the carrier of CLSStruct(# (),(),(),() #)
[V0,(nilfunc * X0)] is set
{V0,(nilfunc * X0)} is non empty set
{V0} is non empty V64() set
{{V0,(nilfunc * X0)},{V0}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [V0,(nilfunc * X0)] is set
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(V0 * nilfunc) (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
nilfunc (#) (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) (nilfunc (#) (X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((nilfunc (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) ((nilfunc (#) (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((nilfunc * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 (#) ((nilfunc * X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
V0 is Element of the carrier of CLSStruct(# (),(),(),() #)
1r * V0 is Element of the carrier of CLSStruct(# (),(),(),() #)
the Mult of CLSStruct(# (),(),(),() #) is Relation-like [:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] -defined the carrier of CLSStruct(# (),(),(),() #) -valued Function-like non empty V14([:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):]
[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
bool [:[:COMPLEX, the carrier of CLSStruct(# (),(),(),() #):], the carrier of CLSStruct(# (),(),(),() #):] is non empty set
[1r,V0] is set
{1r,V0} is non empty set
{1r} is non empty V64() set
{{1r,V0},{1r}} is non empty set
the Mult of CLSStruct(# (),(),(),() #) . [1r,V0] is set
(V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
1r (#) (V0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
() is non empty strict CLSStruct
the carrier of () is non empty set
nilfunc is Element of the carrier of ()
X0 is Element of the carrier of ()
nilfunc + X0 is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (nilfunc,X0) is Element of the carrier of ()
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the addF of () . [nilfunc,X0] is set
seq is Element of the carrier of ()
(nilfunc + X0) + seq is Element of the carrier of ()
the addF of () . ((nilfunc + X0),seq) is Element of the carrier of ()
[(nilfunc + X0),seq] is set
{(nilfunc + X0),seq} is non empty set
{(nilfunc + X0)} is non empty set
{{(nilfunc + X0),seq},{(nilfunc + X0)}} is non empty set
the addF of () . [(nilfunc + X0),seq] is set
X0 + seq is Element of the carrier of ()
the addF of () . (X0,seq) is Element of the carrier of ()
[X0,seq] is set
{X0,seq} is non empty set
{X0} is non empty set
{{X0,seq},{X0}} is non empty set
the addF of () . [X0,seq] is set
nilfunc + (X0 + seq) is Element of the carrier of ()
the addF of () . (nilfunc,(X0 + seq)) is Element of the carrier of ()
[nilfunc,(X0 + seq)] is set
{nilfunc,(X0 + seq)} is non empty set
{{nilfunc,(X0 + seq)},{nilfunc}} is non empty set
the addF of () . [nilfunc,(X0 + seq)] is set
the carrier of () is non empty set
nilfunc is Element of the carrier of ()
0. () is zero Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
nilfunc + (0. ()) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (nilfunc,(0. ())) is Element of the carrier of ()
[nilfunc,(0. ())] is set
{nilfunc,(0. ())} is non empty set
{nilfunc} is non empty set
{{nilfunc,(0. ())},{nilfunc}} is non empty set
the addF of () . [nilfunc,(0. ())] is set
the carrier of () is non empty set
nilfunc is Element of the carrier of ()
0. () is zero Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
X0 is Element of the carrier of ()
nilfunc + X0 is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (nilfunc,X0) is Element of the carrier of ()
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the addF of () . [nilfunc,X0] is set
the carrier of () is non empty set
X0 is Element of the carrier of ()
seq is Element of the carrier of ()
X0 + seq is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (X0,seq) is Element of the carrier of ()
[X0,seq] is set
{X0,seq} is non empty set
{X0} is non empty set
{{X0,seq},{X0}} is non empty set
the addF of () . [X0,seq] is set
nilfunc is complex set
nilfunc * (X0 + seq) is Element of the carrier of ()
the Mult of () is Relation-like [:COMPLEX, the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([:COMPLEX, the carrier of ():]) quasi_total Element of bool [:[:COMPLEX, the carrier of ():], the carrier of ():]
[:COMPLEX, the carrier of ():] is non empty set
[:[:COMPLEX, the carrier of ():], the carrier of ():] is non empty set
bool [:[:COMPLEX, the carrier of ():], the carrier of ():] is non empty set
[nilfunc,(X0 + seq)] is set
{nilfunc,(X0 + seq)} is non empty set
{nilfunc} is non empty V64() set
{{nilfunc,(X0 + seq)},{nilfunc}} is non empty set
the Mult of () . [nilfunc,(X0 + seq)] is set
nilfunc * X0 is Element of the carrier of ()
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the Mult of () . [nilfunc,X0] is set
nilfunc * seq is Element of the carrier of ()
[nilfunc,seq] is set
{nilfunc,seq} is non empty set
{{nilfunc,seq},{nilfunc}} is non empty set
the Mult of () . [nilfunc,seq] is set
(nilfunc * X0) + (nilfunc * seq) is Element of the carrier of ()
the addF of () . ((nilfunc * X0),(nilfunc * seq)) is Element of the carrier of ()
[(nilfunc * X0),(nilfunc * seq)] is set
{(nilfunc * X0),(nilfunc * seq)} is non empty set
{(nilfunc * X0)} is non empty set
{{(nilfunc * X0),(nilfunc * seq)},{(nilfunc * X0)}} is non empty set
the addF of () . [(nilfunc * X0),(nilfunc * seq)] is set
v is Element of the carrier of ()
p is complex set
m is complex set
p + m is complex set
(p + m) * v is Element of the carrier of ()
[(p + m),v] is set
{(p + m),v} is non empty set
{(p + m)} is non empty V64() set
{{(p + m),v},{(p + m)}} is non empty set
the Mult of () . [(p + m),v] is set
p * v is Element of the carrier of ()
[p,v] is set
{p,v} is non empty set
{p} is non empty V64() set
{{p,v},{p}} is non empty set
the Mult of () . [p,v] is set
m * v is Element of the carrier of ()
[m,v] is set
{m,v} is non empty set
{m} is non empty V64() set
{{m,v},{m}} is non empty set
the Mult of () . [m,v] is set
(p * v) + (m * v) is Element of the carrier of ()
the addF of () . ((p * v),(m * v)) is Element of the carrier of ()
[(p * v),(m * v)] is set
{(p * v),(m * v)} is non empty set
{(p * v)} is non empty set
{{(p * v),(m * v)},{(p * v)}} is non empty set
the addF of () . [(p * v),(m * v)] is set
w is Element of the carrier of ()
v1 is complex set
w1 is complex set
v1 * w1 is complex set
(v1 * w1) * w is Element of the carrier of ()
[(v1 * w1),w] is set
{(v1 * w1),w} is non empty set
{(v1 * w1)} is non empty V64() set
{{(v1 * w1),w},{(v1 * w1)}} is non empty set
the Mult of () . [(v1 * w1),w] is set
w1 * w is Element of the carrier of ()
[w1,w] is set
{w1,w} is non empty set
{w1} is non empty V64() set
{{w1,w},{w1}} is non empty set
the Mult of () . [w1,w] is set
v1 * (w1 * w) is Element of the carrier of ()
[v1,(w1 * w)] is set
{v1,(w1 * w)} is non empty set
{v1} is non empty V64() set
{{v1,(w1 * w)},{v1}} is non empty set
the Mult of () . [v1,(w1 * w)] is set
c₁₁ is Element of the carrier of ()
1r * c₁₁ is Element of the carrier of ()
[1r,c₁₁] is set
{1r,c₁₁} is non empty set
{1r} is non empty V64() set
{{1r,c₁₁},{1r}} is non empty set
the Mult of () . [1r,c₁₁] is set
V0 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of V0 is non empty set
bool the carrier of V0 is non empty set
nilfunc is Element of bool the carrier of V0
the addF of V0 is Relation-like [: the carrier of V0, the carrier of V0:] -defined the carrier of V0 -valued Function-like non empty V14([: the carrier of V0, the carrier of V0:]) quasi_total Element of bool [:[: the carrier of V0, the carrier of V0:], the carrier of V0:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:], the carrier of V0:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:], the carrier of V0:] is non empty set
the addF of V0 || nilfunc is Relation-like Function-like set
[:nilfunc,nilfunc:] is set
the addF of V0 | [:nilfunc,nilfunc:] is Relation-like Function-like set
[:[:nilfunc,nilfunc:],nilfunc:] is set
bool [:[:nilfunc,nilfunc:],nilfunc:] is non empty set
dom the addF of V0 is Relation-like set
X0 is set
( the addF of V0 || nilfunc) . X0 is set
seq is set
p is set
[seq,p] is set
{seq,p} is non empty set
{seq} is non empty set
{{seq,p},{seq}} is non empty set
dom ( the addF of V0 || nilfunc) is set
v is right_complementable Element of the carrier of V0
m is right_complementable Element of the carrier of V0
v + m is right_complementable Element of the carrier of V0
the addF of V0 . (v,m) is right_complementable Element of the carrier of V0
[v,m] is set
{v,m} is non empty set
{v} is non empty set
{{v,m},{v}} is non empty set
the addF of V0 . [v,m] is set
dom ( the addF of V0 || nilfunc) is set
V0 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of V0 is non empty set
bool the carrier of V0 is non empty set
nilfunc is Element of bool the carrier of V0
the Mult of V0 is Relation-like [:COMPLEX, the carrier of V0:] -defined the carrier of V0 -valued Function-like non empty V14([:COMPLEX, the carrier of V0:]) quasi_total Element of bool [:[:COMPLEX, the carrier of V0:], the carrier of V0:]
[:COMPLEX, the carrier of V0:] is non empty set
[:[:COMPLEX, the carrier of V0:], the carrier of V0:] is non empty set
bool [:[:COMPLEX, the carrier of V0:], the carrier of V0:] is non empty set
[:COMPLEX,nilfunc:] is set
the Mult of V0 | [:COMPLEX,nilfunc:] is Relation-like Function-like set
[:[:COMPLEX,nilfunc:],nilfunc:] is set
bool [:[:COMPLEX,nilfunc:],nilfunc:] is non empty set
dom the Mult of V0 is Relation-like set
X0 is set
( the Mult of V0 | [:COMPLEX,nilfunc:]) . X0 is set
seq is set
p is set
[seq,p] is set
{seq,p} is non empty set
{seq} is non empty set
{{seq,p},{seq}} is non empty set
m is complex set
[m,p] is set
{m,p} is non empty set
{m} is non empty V64() set
{{m,p},{m}} is non empty set
dom ( the Mult of V0 | [:COMPLEX,nilfunc:]) is set
v is right_complementable Element of the carrier of V0
m * v is right_complementable Element of the carrier of V0
[m,v] is set
{m,v} is non empty set
{{m,v},{m}} is non empty set
the Mult of V0 . [m,v] is set
dom ( the Mult of V0 | [:COMPLEX,nilfunc:]) is set
V0 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of V0 is non empty set
bool the carrier of V0 is non empty set
nilfunc is Element of bool the carrier of V0
0. V0 is zero right_complementable Element of the carrier of V0
the ZeroF of V0 is right_complementable Element of the carrier of V0
the Element of nilfunc is Element of nilfunc
seq is right_complementable Element of the carrier of V0
seq - seq is right_complementable Element of the carrier of V0
- seq is right_complementable Element of the carrier of V0
seq + (- seq) is right_complementable Element of the carrier of V0
the addF of V0 is Relation-like [: the carrier of V0, the carrier of V0:] -defined the carrier of V0 -valued Function-like non empty V14([: the carrier of V0, the carrier of V0:]) quasi_total Element of bool [:[: the carrier of V0, the carrier of V0:], the carrier of V0:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:], the carrier of V0:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:], the carrier of V0:] is non empty set
the addF of V0 . (seq,(- seq)) is right_complementable Element of the carrier of V0
[seq,(- seq)] is set
{seq,(- seq)} is non empty set
{seq} is non empty set
{{seq,(- seq)},{seq}} is non empty set
the addF of V0 . [seq,(- seq)] is set
V0 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of V0 is non empty set
bool the carrier of V0 is non empty set
nilfunc is Element of bool the carrier of V0
(V0,nilfunc) is Element of nilfunc
(V0,nilfunc) is Relation-like [:nilfunc,nilfunc:] -defined nilfunc -valued Function-like quasi_total Element of bool [:[:nilfunc,nilfunc:],nilfunc:]
[:nilfunc,nilfunc:] is set
[:[:nilfunc,nilfunc:],nilfunc:] is set
bool [:[:nilfunc,nilfunc:],nilfunc:] is non empty set
(V0,nilfunc) is Relation-like [:COMPLEX,nilfunc:] -defined nilfunc -valued Function-like quasi_total Element of bool [:[:COMPLEX,nilfunc:],nilfunc:]
[:COMPLEX,nilfunc:] is set
[:[:COMPLEX,nilfunc:],nilfunc:] is set
bool [:[:COMPLEX,nilfunc:],nilfunc:] is non empty set
CLSStruct(# nilfunc,(V0,nilfunc),(V0,nilfunc),(V0,nilfunc) #) is strict CLSStruct
the addF of V0 is Relation-like [: the carrier of V0, the carrier of V0:] -defined the carrier of V0 -valued Function-like non empty V14([: the carrier of V0, the carrier of V0:]) quasi_total Element of bool [:[: the carrier of V0, the carrier of V0:], the carrier of V0:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:], the carrier of V0:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:], the carrier of V0:] is non empty set
the addF of V0 || nilfunc is Relation-like Function-like set
the addF of V0 | [:nilfunc,nilfunc:] is Relation-like Function-like set
the Mult of V0 is Relation-like [:COMPLEX, the carrier of V0:] -defined the carrier of V0 -valued Function-like non empty V14([:COMPLEX, the carrier of V0:]) quasi_total Element of bool [:[:COMPLEX, the carrier of V0:], the carrier of V0:]
[:COMPLEX, the carrier of V0:] is non empty set
[:[:COMPLEX, the carrier of V0:], the carrier of V0:] is non empty set
bool [:[:COMPLEX, the carrier of V0:], the carrier of V0:] is non empty set
the Mult of V0 | [:COMPLEX,nilfunc:] is Relation-like Function-like set
0. V0 is zero right_complementable Element of the carrier of V0
the ZeroF of V0 is right_complementable Element of the carrier of V0
the carrier of () is non empty set
bool the carrier of () is non empty set
V0 is set
nilfunc is set
bool () is non empty set
(()) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
|.(()).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
|.(()).| (#) |.(()).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
nilfunc is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
X0 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
nilfunc . X0 is complex V34() ext-real Element of REAL
|.(()).| . X0 is complex V34() ext-real Element of REAL
(|.(()).| . X0) * (|.(()).| . X0) is complex V34() ext-real Element of REAL
(()) . X0 is complex Element of COMPLEX
|.((()) . X0).| is complex V34() ext-real Element of REAL
(|.(()).| . X0) * |.((()) . X0).| is complex V34() ext-real Element of REAL
(|.(()).| . X0) * 0 is complex V34() ext-real Element of REAL
V0 is Element of bool the carrier of ()
nilfunc is Element of bool the carrier of ()
X0 is set
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
|.(X0).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
|.(X0).| (#) |.(X0).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
X0 is set
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
|.(X0).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
|.(X0).| (#) |.(X0).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
() is Element of bool the carrier of ()
nilfunc is right_complementable Element of the carrier of ()
X0 is right_complementable Element of the carrier of ()
nilfunc + X0 is right_complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (nilfunc,X0) is right_complementable Element of the carrier of ()
[nilfunc,X0] is set
{nilfunc,X0} is non empty set
{nilfunc} is non empty set
{{nilfunc,X0},{nilfunc}} is non empty set
the addF of () . [nilfunc,X0] is set
((nilfunc + X0)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
|.((nilfunc + X0)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
|.((nilfunc + X0)).| (#) |.((nilfunc + X0)).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
(X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
|.(X0).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
|.(X0).| (#) |.(X0).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
(nilfunc) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
|.(nilfunc).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
|.(nilfunc).| (#) |.(nilfunc).| is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
v is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.((nilfunc + X0)).| (#) |.((nilfunc + X0)).|) . v is complex V34() ext-real Element of REAL
|.((nilfunc + X0)).| . v is complex V34() ext-real Element of REAL
(|.((nilfunc + X0)).| . v) * (|.((nilfunc + X0)).| . v) is complex V34() ext-real Element of REAL
2 is non empty V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 (#) (|.(nilfunc).| (#) |.(nilfunc).|) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
2 (#) (|.(X0).| (#) |.(X0).|) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
(2 (#) (|.(nilfunc).| (#) |.(nilfunc).|)) + (2 (#) (|.(X0).| (#) |.(X0).|)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V38() V39() V40() Element of bool [:NAT,REAL:]
w1 is V26() V27() V28() V32() complex V34() ext-real V50() V63() V64() V65() V66() V67() V68() V69() Element of NAT
(|.((nilfunc + X0)).| (#) |.((nilfunc + X0)).|) . w1 is complex V34() ext-real Element of REAL
((2 (#) (|.(nilfunc).| (#) |.(nilfunc).|)) + (2 (#) (|.(X0).| (#) |.(X0).|))) . w1 is complex V34() ext-real Element of REAL
|.(nilfunc).| . w1 is complex V34() ext-real Element of REAL
|.(X0).| . w1 is complex V34() ext-real Element of REAL
|.((nilfunc + X0)).| . w1 is complex V34() ext-real Element of REAL
(|.((nilfunc + X0)).| . w1) ^2 is complex V34() ext-real Element of REAL
(|.((nilfunc + X0)).| . w1) * (|.((nilfunc + X0)).| . w1) is complex set
(2 (#) (|.(nilfunc).| (#) |.(nilfunc).|)) . w1 is complex V34() ext-real Element of REAL
(2 (#) (|.(X0).| (#) |.(X0).|)) . w1 is complex V34() ext-real Element of REAL
((2 (#) (|.(nilfunc).| (#) |.(nilfunc).|)) . w1) + ((2 (#) (|.(X0).| (#) |.(X0).|)) . w1) is complex V34() ext-real Element of REAL
(|.(nilfunc).| (#) |.(nilfunc).|) . w1 is complex V34() ext-real Element of REAL
2 * ((|.(nilfunc).| (#) |.(nilfunc).|) . w1) is complex V34() ext-real Element of REAL
(2 * ((|.(nilfunc).| (#) |.(nilfunc).|) . w1)) + ((2 (#) (|.(X0).| (#) |.(X0).|)) . w1) is complex V34() ext-real Element of REAL
(|.(X0).| (#) |.(X0).|) . w1 is complex V34() ext-real Element of REAL
2 * ((|.(X0).| (#) |.(X0).|) . w1) is complex V34() ext-real Element of REAL
(2 * ((|.(nilfunc).| (#) |.(nilfunc).|) . w1)) + (2 * ((|.(X0).| (#) |.(X0).|) . w1)) is complex V34() ext-real Element of REAL
(|.(nilfunc).| . w1) * (|.(nilfunc).| . w1) is complex V34() ext-real Element of REAL
2 * ((|.(nilfunc).| . w1) * (|.(nilfunc).| . w1)) is complex V34() ext-real Element of REAL
(2 * ((|.(nilfunc).| . w1) * (|.(nilfunc).| . w1))) + (2 * ((|.(X0).| (#) |.(X0).|) . w1)) is complex V34() ext-real Element of REAL
w is complex V34() ext-real Element of REAL
w ^2 is complex V34() ext-real Element of REAL
w * w is complex set
2 * (w ^2) is complex V34() ext-real Element of REAL
c₁₁ is complex V34() ext-real Element of REAL
c₁₁ ^2 is complex V34() ext-real Element of REAL
c₁₁ * c₁₁ is complex set
2 * (c₁₁ ^2) is complex V34() ext-real Element of REAL
(2 * (w ^2)) + (2 * (c₁₁ ^2)) is complex V34() ext-real Element of REAL
2 * w is complex V34() ext-real Element of REAL
(2 * w) * c₁₁ is complex V34() ext-real Element of REAL
(w ^2) + ((2 * w) * c₁₁) is complex V34() ext-real Element of REAL
((w ^2) + ((2 * w) * c₁₁)) + (c₁₁ ^2) is complex V34() ext-real Element of REAL
(((2 (#) (|.(nilfunc).| (#) |.(nilfunc).|)) + (2 (#) (|.(X0).| (#) |.(X0).|))) . w1) - (((w ^2) + ((2 * w) * c₁₁)) + (c₁₁ ^2)) is complex V34() ext-real Element of REAL
w - c₁₁ is complex V34() ext-real Element of REAL
(w - c₁₁) ^2 is complex V34() ext-real Element of REAL
(w - c₁₁) * (w - c₁₁) is complex set
(nilfunc) + (X0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
(((nilfunc) + (X0))) is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) quasi_total V38() Element of bool [:NAT,COMPLEX:]
((nilfunc + X0)) . w1 is complex Element of COMPLEX
|.(((nilfunc + X0)) . w1).| is complex V34() ext-real Element of REAL
(nilfunc) . w1 is complex Element of COMPLEX
(X0) . w1 is complex Element of COMPLEX
((nilfunc) . w1) + ((X0) . w1) is complex Element of COMPLEX
|.(((nilfunc) . w1) + ((X0) . w1)).| is complex V34() ext-real Element of REAL
|.((nilfunc) . w1).| is complex V34() ext-real Element of REAL
|.((X0) . w1).| is complex V34() ext-real Element of REAL
|.((nilfunc) . w1).| + |.((X0) . w1).| is complex V34() ext-real Element of REAL
(|.(nilfunc).| . w1) + |.((X0) . w1).| is complex V34() ext-real Element of REAL
(|.(nilfunc).| . w1) + (|.(X0).| . w1) is complex V34() ext-real Element of REAL
0 + (((w ^2) + ((2 * w) * c₁₁)) + (c₁₁ ^2)) is complex V34() ext-real Element of REAL
((|.(nilfunc).| . w1) + (|.(X0).| . w1)) ^2 is complex V34() ext-real Element of REAL
((|.(nilfunc).| . w1) + (|.(X0).| . w1)) * ((|.(nilfunc).| . w1) + (|.(X0).| . w1)) is complex set
nilfunc is complex set
X0 is right_complementable Element of the carrier of ()
nilfunc * X0 is right_complementable Element of the carrier of ()
the Mult of () is Relation-like [:COMPLEX, the carrier of ():] -defined the carrier of () -valued Function-like non empty V14([:COMPLEX, the carrier of ():]) quasi_total Element of bool [:[:COMPLEX, the carrier of ():], the carrier of ():]
[:COMPLEX, the carrier of ():] is non empty set