:: HERMITAN semantic presentation

REAL is non empty V38() V175() V176() V177() V181() set
NAT is V175() V176() V177() V178() V179() V180() V181() Element of bool REAL
bool REAL is set
F_Complex is non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital V137() V139() right-distributive left-distributive right_unital well-unital V145() left_unital doubleLoopStr
the carrier of F_Complex is non empty non trivial set
COMPLEX is non empty V38() V175() V181() set
RAT is non empty V38() V175() V176() V177() V178() V181() set
INT is non empty V38() V175() V176() V177() V178() V179() V181() set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
omega is V175() V176() V177() V178() V179() V180() V181() set
bool omega is set
K270() is L6()
the carrier of K270() is set
bool NAT is set
ExtREAL is non empty V176() set
{} is empty V175() V176() V177() V178() V179() V180() V181() set
the empty V175() V176() V177() V178() V179() V180() V181() set is empty V175() V176() V177() V178() V179() V180() V181() set
1 is non empty natural complex real ext-real positive non negative V33() V34() V175() V176() V177() V178() V179() V180() Element of NAT
2 is non empty natural complex real ext-real positive non negative V33() V34() V175() V176() V177() V178() V179() V180() Element of NAT
[:2,REAL:] is set
bool [:2,REAL:] is set
0 is empty natural complex real ext-real non positive non negative V33() V34() V175() V176() V177() V178() V179() V180() V181() Element of NAT
Re 0 is complex real ext-real Element of REAL
Im 0 is complex real ext-real Element of REAL
<i> is complex Element of COMPLEX
Re <i> is complex real ext-real Element of REAL
Im <i> is complex real ext-real Element of REAL
|.0.| is complex real ext-real Element of REAL
(Re 0) ^2 is complex real ext-real Element of REAL
(Re 0) * (Re 0) is complex real ext-real set
(Im 0) ^2 is complex real ext-real Element of REAL
(Im 0) * (Im 0) is complex real ext-real set
((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL
sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL
1r is complex Element of COMPLEX
|.1r.| is complex real ext-real Element of REAL
Re 1r is complex real ext-real Element of REAL
(Re 1r) ^2 is complex real ext-real Element of REAL
(Re 1r) * (Re 1r) is complex real ext-real set
Im 1r is complex real ext-real Element of REAL
(Im 1r) ^2 is complex real ext-real Element of REAL
(Im 1r) * (Im 1r) is complex real ext-real set
((Re 1r) ^2) + ((Im 1r) ^2) is complex real ext-real Element of REAL
sqrt (((Re 1r) ^2) + ((Im 1r) ^2)) is complex real ext-real Element of REAL
sqrt 1 is complex real ext-real Element of REAL
K159() is V16() V19([:COMPLEX,COMPLEX:]) V20( COMPLEX ) Function-like V30([:COMPLEX,COMPLEX:], COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
K161() is V16() V19([:COMPLEX,COMPLEX:]) V20( COMPLEX ) Function-like V30([:COMPLEX,COMPLEX:], COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
0c is empty complex V175() V176() V177() V178() V179() V180() V181() Element of COMPLEX
0. F_Complex is complex zero Element of the carrier of F_Complex
1_ F_Complex is complex Element of the carrier of F_Complex
1. F_Complex is complex non zero Element of the carrier of F_Complex
(0. F_Complex) *' is complex Element of the carrier of F_Complex
Re (0. F_Complex) is complex real ext-real Element of REAL
Im (0. F_Complex) is complex real ext-real Element of REAL
(Im (0. F_Complex)) * <i> is complex set
(Re (0. F_Complex)) - ((Im (0. F_Complex)) * <i>) is complex set
(1. F_Complex) *' is complex Element of the carrier of F_Complex
Re (1. F_Complex) is complex real ext-real Element of REAL
Im (1. F_Complex) is complex real ext-real Element of REAL
(Im (1. F_Complex)) * <i> is complex set
(Re (1. F_Complex)) - ((Im (1. F_Complex)) * <i>) is complex set
|.(0. F_Complex).| is complex real ext-real Element of REAL
(Re (0. F_Complex)) ^2 is complex real ext-real Element of REAL
(Re (0. F_Complex)) * (Re (0. F_Complex)) is complex real ext-real set
(Im (0. F_Complex)) ^2 is complex real ext-real Element of REAL
(Im (0. F_Complex)) * (Im (0. F_Complex)) is complex real ext-real set
((Re (0. F_Complex)) ^2) + ((Im (0. F_Complex)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (0. F_Complex)) ^2) + ((Im (0. F_Complex)) ^2)) is complex real ext-real Element of REAL
|.(1. F_Complex).| is complex real ext-real Element of REAL
(Re (1. F_Complex)) ^2 is complex real ext-real Element of REAL
(Re (1. F_Complex)) * (Re (1. F_Complex)) is complex real ext-real set
(Im (1. F_Complex)) ^2 is complex real ext-real Element of REAL
(Im (1. F_Complex)) * (Im (1. F_Complex)) is complex real ext-real set
((Re (1. F_Complex)) ^2) + ((Im (1. F_Complex)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (1. F_Complex)) ^2) + ((Im (1. F_Complex)) ^2)) is complex real ext-real Element of REAL
i_FC is complex Element of the carrier of F_Complex
i_FC * i_FC is complex Element of the carrier of F_Complex
the multF of F_Complex is V16() V19([: the carrier of F_Complex, the carrier of F_Complex:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
the multF of F_Complex . (i_FC,i_FC) is complex Element of the carrier of F_Complex
[i_FC,i_FC] is set
{i_FC,i_FC} is non empty V175() set
{i_FC} is non empty V175() set
{{i_FC,i_FC},{i_FC}} is non empty set
the multF of F_Complex . [i_FC,i_FC] is set
K137(i_FC,i_FC) is complex Element of COMPLEX
- (1_ F_Complex) is complex Element of the carrier of F_Complex
0 * <i> is complex set
0 + (0 * <i>) is complex set
V is complex set
V *' is complex Element of COMPLEX
Re V is complex real ext-real Element of REAL
Im V is complex real ext-real Element of REAL
(Im V) * <i> is complex set
(Re V) - ((Im V) * <i>) is complex set
- (Im V) is complex real ext-real Element of REAL
0 + (- (Im V)) is complex real ext-real Element of REAL
V is complex Element of COMPLEX
Re V is complex real ext-real Element of REAL
|.V.| is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
Im V is complex real ext-real Element of REAL
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
(Re V) / |.V.| is complex real ext-real Element of COMPLEX
- (Im V) is complex real ext-real Element of REAL
(- (Im V)) / |.V.| is complex real ext-real Element of COMPLEX
((- (Im V)) / |.V.|) * <i> is complex Element of COMPLEX
((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>) is complex Element of COMPLEX
|.(((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)).| is complex real ext-real Element of REAL
Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) is complex real ext-real Element of REAL
(Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2 is complex real ext-real Element of REAL
(Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) * (Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) is complex real ext-real set
Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) is complex real ext-real Element of REAL
(Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2 is complex real ext-real Element of REAL
(Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) * (Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) is complex real ext-real set
((Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2) + ((Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2) + ((Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2)) is complex real ext-real Element of REAL
(((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * V is complex Element of COMPLEX
Re ((((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * V) is complex real ext-real Element of REAL
Im ((((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * V) is complex real ext-real Element of REAL
V * V is complex Element of COMPLEX
|.(V * V).| is complex real ext-real Element of REAL
Re (V * V) is complex real ext-real Element of REAL
(Re (V * V)) ^2 is complex real ext-real Element of REAL
(Re (V * V)) * (Re (V * V)) is complex real ext-real set
Im (V * V) is complex real ext-real Element of REAL
(Im (V * V)) ^2 is complex real ext-real Element of REAL
(Im (V * V)) * (Im (V * V)) is complex real ext-real set
((Re (V * V)) ^2) + ((Im (V * V)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (V * V)) ^2) + ((Im (V * V)) ^2)) is complex real ext-real Element of REAL
|.V.| ^2 is complex real ext-real Element of REAL
|.V.| * |.V.| is complex real ext-real set
((Re V) ^2) / (|.V.| ^2) is complex real ext-real Element of COMPLEX
((- (Im V)) / |.V.|) ^2 is complex real ext-real Element of COMPLEX
((- (Im V)) / |.V.|) * ((- (Im V)) / |.V.|) is complex real ext-real set
(((Re V) ^2) / (|.V.| ^2)) + (((- (Im V)) / |.V.|) ^2) is complex real ext-real Element of COMPLEX
(- (Im V)) ^2 is complex real ext-real Element of REAL
(- (Im V)) * (- (Im V)) is complex real ext-real set
((- (Im V)) ^2) / (|.V.| ^2) is complex real ext-real Element of COMPLEX
(((Re V) ^2) / (|.V.| ^2)) + (((- (Im V)) ^2) / (|.V.| ^2)) is complex real ext-real Element of COMPLEX
(((Re V) ^2) + ((Im V) ^2)) / (|.V.| ^2) is complex real ext-real Element of COMPLEX
|.V.| / |.V.| is complex real ext-real Element of COMPLEX
(|.V.| / |.V.|) ^2 is complex real ext-real Element of COMPLEX
(|.V.| / |.V.|) * (|.V.| / |.V.|) is complex real ext-real set
1 ^2 is complex real ext-real Element of REAL
1 * 1 is non empty complex real ext-real positive non negative set
((Re V) / |.V.|) * (Re V) is complex real ext-real Element of REAL
((- (Im V)) / |.V.|) * (Im V) is complex real ext-real Element of REAL
(((Re V) / |.V.|) * (Re V)) - (((- (Im V)) / |.V.|) * (Im V)) is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real Element of REAL
((Re V) * (Re V)) / |.V.| is complex real ext-real Element of COMPLEX
(((Re V) * (Re V)) / |.V.|) - (((- (Im V)) / |.V.|) * (Im V)) is complex real ext-real Element of REAL
((Re V) ^2) / |.V.| is complex real ext-real Element of COMPLEX
(- (Im V)) * (Im V) is complex real ext-real Element of REAL
((- (Im V)) * (Im V)) / |.V.| is complex real ext-real Element of COMPLEX
(((Re V) ^2) / |.V.|) - (((- (Im V)) * (Im V)) / |.V.|) is complex real ext-real Element of COMPLEX
(Im V) * (Im V) is complex real ext-real Element of REAL
- ((Im V) * (Im V)) is complex real ext-real Element of REAL
((Re V) ^2) - (- ((Im V) * (Im V))) is complex real ext-real Element of REAL
(((Re V) ^2) - (- ((Im V) * (Im V)))) / |.V.| is complex real ext-real Element of COMPLEX
((Re V) / |.V.|) * (Im V) is complex real ext-real Element of REAL
(Re V) * ((- (Im V)) / |.V.|) is complex real ext-real Element of REAL
(((Re V) / |.V.|) * (Im V)) + ((Re V) * ((- (Im V)) / |.V.|)) is complex real ext-real Element of REAL
(Re V) * (Im V) is complex real ext-real Element of REAL
((Re V) * (Im V)) / |.V.| is complex real ext-real Element of COMPLEX
(((Re V) * (Im V)) / |.V.|) + ((Re V) * ((- (Im V)) / |.V.|)) is complex real ext-real Element of REAL
(- (Im V)) * (Re V) is complex real ext-real Element of REAL
((- (Im V)) * (Re V)) / |.V.| is complex real ext-real Element of COMPLEX
(((Re V) * (Im V)) / |.V.|) + (((- (Im V)) * (Re V)) / |.V.|) is complex real ext-real Element of COMPLEX
(Im V) * (Re V) is complex real ext-real Element of REAL
- ((Im V) * (Re V)) is complex real ext-real Element of REAL
((Re V) * (Im V)) + (- ((Im V) * (Re V))) is complex real ext-real Element of REAL
(((Re V) * (Im V)) + (- ((Im V) * (Re V)))) / |.V.| is complex real ext-real Element of COMPLEX
V is complex Element of COMPLEX
|.V.| is complex real ext-real Element of REAL
Re V is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
Im V is complex real ext-real Element of REAL
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
1r * V is complex Element of COMPLEX
Re (1r * V) is complex real ext-real Element of REAL
Im (1r * V) is complex real ext-real Element of REAL
(Re V) / |.V.| is complex real ext-real Element of COMPLEX
- (Im V) is complex real ext-real Element of REAL
(- (Im V)) / |.V.| is complex real ext-real Element of COMPLEX
((- (Im V)) / |.V.|) * <i> is complex Element of COMPLEX
((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>) is complex Element of COMPLEX
|.(((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)).| is complex real ext-real Element of REAL
Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) is complex real ext-real Element of REAL
(Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2 is complex real ext-real Element of REAL
(Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) * (Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) is complex real ext-real set
Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) is complex real ext-real Element of REAL
(Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2 is complex real ext-real Element of REAL
(Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) * (Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) is complex real ext-real set
((Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2) + ((Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2) + ((Im (((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>))) ^2)) is complex real ext-real Element of REAL
(((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * V is complex Element of COMPLEX
Re ((((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * V) is complex real ext-real Element of REAL
Im ((((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * V) is complex real ext-real Element of REAL
vq is complex Element of COMPLEX
|.vq.| is complex real ext-real Element of REAL
Re vq is complex real ext-real Element of REAL
(Re vq) ^2 is complex real ext-real Element of REAL
(Re vq) * (Re vq) is complex real ext-real set
Im vq is complex real ext-real Element of REAL
(Im vq) ^2 is complex real ext-real Element of REAL
(Im vq) * (Im vq) is complex real ext-real set
((Re vq) ^2) + ((Im vq) ^2) is complex real ext-real Element of REAL
sqrt (((Re vq) ^2) + ((Im vq) ^2)) is complex real ext-real Element of REAL
vq * V is complex Element of COMPLEX
Re (vq * V) is complex real ext-real Element of REAL
Im (vq * V) is complex real ext-real Element of REAL
vr is complex Element of COMPLEX
|.vr.| is complex real ext-real Element of REAL
Re vr is complex real ext-real Element of REAL
(Re vr) ^2 is complex real ext-real Element of REAL
(Re vr) * (Re vr) is complex real ext-real set
Im vr is complex real ext-real Element of REAL
(Im vr) ^2 is complex real ext-real Element of REAL
(Im vr) * (Im vr) is complex real ext-real set
((Re vr) ^2) + ((Im vr) ^2) is complex real ext-real Element of REAL
sqrt (((Re vr) ^2) + ((Im vr) ^2)) is complex real ext-real Element of REAL
vr * V is complex Element of COMPLEX
Re (vr * V) is complex real ext-real Element of REAL
Im (vr * V) is complex real ext-real Element of REAL
V is complex Element of COMPLEX
V *' is complex Element of COMPLEX
Re V is complex real ext-real Element of REAL
Im V is complex real ext-real Element of REAL
(Im V) * <i> is complex set
(Re V) - ((Im V) * <i>) is complex set
V * (V *') is complex Element of COMPLEX
|.V.| is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
|.V.| ^2 is complex real ext-real Element of REAL
|.V.| * |.V.| is complex real ext-real set
(|.V.| ^2) + (0 * <i>) is complex set
Re (V * (V *')) is complex real ext-real Element of REAL
Im (V * (V *')) is complex real ext-real Element of REAL
V is complex Element of the carrier of F_Complex
V *' is complex Element of the carrier of F_Complex
Re V is complex real ext-real Element of REAL
Im V is complex real ext-real Element of REAL
(Im V) * <i> is complex set
(Re V) - ((Im V) * <i>) is complex set
i_FC *' is complex Element of the carrier of F_Complex
Re i_FC is complex real ext-real Element of REAL
Im i_FC is complex real ext-real Element of REAL
(Im i_FC) * <i> is complex set
(Re i_FC) - ((Im i_FC) * <i>) is complex set
i_FC * (i_FC *') is complex Element of the carrier of F_Complex
the multF of F_Complex . (i_FC,(i_FC *')) is complex Element of the carrier of F_Complex
[i_FC,(i_FC *')] is set
{i_FC,(i_FC *')} is non empty V175() set
{{i_FC,(i_FC *')},{i_FC}} is non empty set
the multF of F_Complex . [i_FC,(i_FC *')] is set
K137(i_FC,(i_FC *')) is complex Element of COMPLEX
V is complex Element of the carrier of F_Complex
Re V is complex real ext-real Element of REAL
|.V.| is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
Im V is complex real ext-real Element of REAL
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
(Re V) / |.V.| is complex real ext-real Element of COMPLEX
- (Im V) is complex real ext-real Element of REAL
(- (Im V)) / |.V.| is complex real ext-real Element of COMPLEX
[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] is complex Element of the carrier of F_Complex
((- (Im V)) / |.V.|) * <i> is complex set
((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>) is complex set
|.[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**].| is complex real ext-real Element of REAL
Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] is complex real ext-real Element of REAL
(Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2 is complex real ext-real Element of REAL
(Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) * (Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) is complex real ext-real set
Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] is complex real ext-real Element of REAL
(Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2 is complex real ext-real Element of REAL
(Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) * (Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) is complex real ext-real set
((Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2) + ((Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2) is complex real ext-real Element of REAL
sqrt (((Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2) + ((Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2)) is complex real ext-real Element of REAL
[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] * V is complex Element of the carrier of F_Complex
the multF of F_Complex . ([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V) is complex Element of the carrier of F_Complex
[[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V] is set
{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V} is non empty V175() set
{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]} is non empty V175() set
{{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V},{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]}} is non empty set
the multF of F_Complex . [[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V] is set
K137([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V) is complex Element of COMPLEX
Re ([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] * V) is complex real ext-real Element of REAL
Im ([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] * V) is complex real ext-real Element of REAL
((- (Im V)) / |.V.|) * <i> is complex Element of COMPLEX
((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>) is complex Element of COMPLEX
f is complex Element of COMPLEX
(((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>)) * f is complex Element of COMPLEX
V is complex Element of the carrier of F_Complex
|.V.| is complex real ext-real Element of REAL
Re V is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
Im V is complex real ext-real Element of REAL
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
vq is complex non zero Element of the carrier of F_Complex
|.vq.| is complex real ext-real Element of REAL
Re vq is complex real ext-real Element of REAL
(Re vq) ^2 is complex real ext-real Element of REAL
(Re vq) * (Re vq) is complex real ext-real set
Im vq is complex real ext-real Element of REAL
(Im vq) ^2 is complex real ext-real Element of REAL
(Im vq) * (Im vq) is complex real ext-real set
((Re vq) ^2) + ((Im vq) ^2) is complex real ext-real Element of REAL
sqrt (((Re vq) ^2) + ((Im vq) ^2)) is complex real ext-real Element of REAL
vq * V is complex Element of the carrier of F_Complex
the multF of F_Complex . (vq,V) is complex Element of the carrier of F_Complex
[vq,V] is set
{vq,V} is non empty V175() set
{vq} is non empty V175() set
{{vq,V},{vq}} is non empty set
the multF of F_Complex . [vq,V] is set
K137(vq,V) is complex Element of COMPLEX
Re (vq * V) is complex real ext-real Element of REAL
Im (vq * V) is complex real ext-real Element of REAL
(Re V) / |.V.| is complex real ext-real Element of COMPLEX
- (Im V) is complex real ext-real Element of REAL
(- (Im V)) / |.V.| is complex real ext-real Element of COMPLEX
[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] is complex Element of the carrier of F_Complex
((- (Im V)) / |.V.|) * <i> is complex set
((Re V) / |.V.|) + (((- (Im V)) / |.V.|) * <i>) is complex set
|.[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**].| is complex real ext-real Element of REAL
Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] is complex real ext-real Element of REAL
(Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2 is complex real ext-real Element of REAL
(Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) * (Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) is complex real ext-real set
Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] is complex real ext-real Element of REAL
(Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2 is complex real ext-real Element of REAL
(Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) * (Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) is complex real ext-real set
((Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2) + ((Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2) is complex real ext-real Element of REAL
sqrt (((Re [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2) + ((Im [**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]) ^2)) is complex real ext-real Element of REAL
[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] * V is complex Element of the carrier of F_Complex
the multF of F_Complex . ([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V) is complex Element of the carrier of F_Complex
[[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V] is set
{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V} is non empty V175() set
{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]} is non empty V175() set
{{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V},{[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**]}} is non empty set
the multF of F_Complex . [[**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V] is set
K137([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**],V) is complex Element of COMPLEX
Re ([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] * V) is complex real ext-real Element of REAL
Im ([**((Re V) / |.V.|),((- (Im V)) / |.V.|)**] * V) is complex real ext-real Element of REAL
vq is complex Element of the carrier of F_Complex
|.vq.| is complex real ext-real Element of REAL
Re vq is complex real ext-real Element of REAL
(Re vq) ^2 is complex real ext-real Element of REAL
(Re vq) * (Re vq) is complex real ext-real set
Im vq is complex real ext-real Element of REAL
(Im vq) ^2 is complex real ext-real Element of REAL
(Im vq) * (Im vq) is complex real ext-real set
((Re vq) ^2) + ((Im vq) ^2) is complex real ext-real Element of REAL
sqrt (((Re vq) ^2) + ((Im vq) ^2)) is complex real ext-real Element of REAL
vq * V is complex Element of the carrier of F_Complex
the multF of F_Complex . (vq,V) is complex Element of the carrier of F_Complex
[vq,V] is set
{vq,V} is non empty V175() set
{vq} is non empty V175() set
{{vq,V},{vq}} is non empty set
the multF of F_Complex . [vq,V] is set
K137(vq,V) is complex Element of COMPLEX
Re (vq * V) is complex real ext-real Element of REAL
Im (vq * V) is complex real ext-real Element of REAL
vr is complex Element of the carrier of F_Complex
|.vr.| is complex real ext-real Element of REAL
Re vr is complex real ext-real Element of REAL
(Re vr) ^2 is complex real ext-real Element of REAL
(Re vr) * (Re vr) is complex real ext-real set
Im vr is complex real ext-real Element of REAL
(Im vr) ^2 is complex real ext-real Element of REAL
(Im vr) * (Im vr) is complex real ext-real set
((Re vr) ^2) + ((Im vr) ^2) is complex real ext-real Element of REAL
sqrt (((Re vr) ^2) + ((Im vr) ^2)) is complex real ext-real Element of REAL
vr * V is complex Element of the carrier of F_Complex
the multF of F_Complex . (vr,V) is complex Element of the carrier of F_Complex
[vr,V] is set
{vr,V} is non empty V175() set
{vr} is non empty V175() set
{{vr,V},{vr}} is non empty set
the multF of F_Complex . [vr,V] is set
K137(vr,V) is complex Element of COMPLEX
Re (vr * V) is complex real ext-real Element of REAL
Im (vr * V) is complex real ext-real Element of REAL
V is complex Element of the carrier of F_Complex
f is complex Element of the carrier of F_Complex
V - f is complex Element of the carrier of F_Complex
- f is complex Element of the carrier of F_Complex
V + (- f) is complex Element of the carrier of F_Complex
the addF of F_Complex is V16() V19([: the carrier of F_Complex, the carrier of F_Complex:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
the addF of F_Complex . (V,(- f)) is complex Element of the carrier of F_Complex
[V,(- f)] is set
{V,(- f)} is non empty V175() set
{V} is non empty V175() set
{{V,(- f)},{V}} is non empty set
the addF of F_Complex . [V,(- f)] is set
K135(V,(- f)) is complex Element of COMPLEX
Re (V - f) is complex real ext-real Element of REAL
Re V is complex real ext-real Element of REAL
Re f is complex real ext-real Element of REAL
(Re V) - (Re f) is complex real ext-real Element of REAL
Im (V - f) is complex real ext-real Element of REAL
Im V is complex real ext-real Element of REAL
Im f is complex real ext-real Element of REAL
(Im V) - (Im f) is complex real ext-real Element of REAL
vq is complex Element of COMPLEX
vr is complex Element of COMPLEX
vq - vr is complex Element of COMPLEX
Re (vq - vr) is complex real ext-real Element of REAL
Im (vq - vr) is complex real ext-real Element of REAL
V is complex Element of the carrier of F_Complex
Im V is complex real ext-real Element of REAL
f is complex Element of the carrier of F_Complex
V * f is complex Element of the carrier of F_Complex
the multF of F_Complex . (V,f) is complex Element of the carrier of F_Complex
[V,f] is set
{V,f} is non empty V175() set
{V} is non empty V175() set
{{V,f},{V}} is non empty set
the multF of F_Complex . [V,f] is set
K137(V,f) is complex Element of COMPLEX
Re (V * f) is complex real ext-real Element of REAL
Re V is complex real ext-real Element of REAL
Re f is complex real ext-real Element of REAL
(Re V) * (Re f) is complex real ext-real Element of REAL
Im (V * f) is complex real ext-real Element of REAL
Im f is complex real ext-real Element of REAL
(Re V) * (Im f) is complex real ext-real Element of REAL
0 * (Im f) is complex real ext-real Element of REAL
((Re V) * (Re f)) - (0 * (Im f)) is complex real ext-real Element of REAL
(Re f) * 0 is complex real ext-real Element of REAL
((Re V) * (Im f)) + ((Re f) * 0) is complex real ext-real Element of REAL
V is complex Element of the carrier of F_Complex
Im V is complex real ext-real Element of REAL
f is complex Element of the carrier of F_Complex
Im f is complex real ext-real Element of REAL
V * f is complex Element of the carrier of F_Complex
the multF of F_Complex . (V,f) is complex Element of the carrier of F_Complex
[V,f] is set
{V,f} is non empty V175() set
{V} is non empty V175() set
{{V,f},{V}} is non empty set
the multF of F_Complex . [V,f] is set
K137(V,f) is complex Element of COMPLEX
Im (V * f) is complex real ext-real Element of REAL
Re f is complex real ext-real Element of REAL
(Re f) * 0 is complex real ext-real Element of REAL
V is complex Element of the carrier of F_Complex
Im V is complex real ext-real Element of REAL
V *' is complex Element of the carrier of F_Complex
Re V is complex real ext-real Element of REAL
(Im V) * <i> is complex set
(Re V) - ((Im V) * <i>) is complex set
f is complex Element of COMPLEX
Re f is complex real ext-real Element of REAL
Im f is complex real ext-real Element of REAL
- (Im f) is complex real ext-real Element of REAL
(- (Im f)) * <i> is complex set
(Re f) + ((- (Im f)) * <i>) is complex set
V is complex Element of the carrier of F_Complex
V *' is complex Element of the carrier of F_Complex
Re V is complex real ext-real Element of REAL
Im V is complex real ext-real Element of REAL
(Im V) * <i> is complex set
(Re V) - ((Im V) * <i>) is complex set
V * (V *') is complex Element of the carrier of F_Complex
the multF of F_Complex . (V,(V *')) is complex Element of the carrier of F_Complex
[V,(V *')] is set
{V,(V *')} is non empty V175() set
{V} is non empty V175() set
{{V,(V *')},{V}} is non empty set
the multF of F_Complex . [V,(V *')] is set
K137(V,(V *')) is complex Element of COMPLEX
|.V.| is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
|.V.| ^2 is complex real ext-real Element of REAL
|.V.| * |.V.| is complex real ext-real set
f is complex Element of COMPLEX
|.f.| is complex real ext-real Element of REAL
Re f is complex real ext-real Element of REAL
(Re f) ^2 is complex real ext-real Element of REAL
(Re f) * (Re f) is complex real ext-real set
Im f is complex real ext-real Element of REAL
(Im f) ^2 is complex real ext-real Element of REAL
(Im f) * (Im f) is complex real ext-real set
((Re f) ^2) + ((Im f) ^2) is complex real ext-real Element of REAL
sqrt (((Re f) ^2) + ((Im f) ^2)) is complex real ext-real Element of REAL
|.f.| ^2 is complex real ext-real Element of REAL
|.f.| * |.f.| is complex real ext-real set
(|.f.| ^2) + (0 * <i>) is complex set
V is complex Element of the carrier of F_Complex
Re V is complex real ext-real Element of REAL
Im V is complex real ext-real Element of REAL
|.V.| is complex real ext-real Element of REAL
(Re V) ^2 is complex real ext-real Element of REAL
(Re V) * (Re V) is complex real ext-real set
(Im V) ^2 is complex real ext-real Element of REAL
(Im V) * (Im V) is complex real ext-real set
((Re V) ^2) + ((Im V) ^2) is complex real ext-real Element of REAL
sqrt (((Re V) ^2) + ((Im V) ^2)) is complex real ext-real Element of REAL
f is complex Element of COMPLEX
|.f.| is complex real ext-real Element of REAL
Re f is complex real ext-real Element of REAL
(Re f) ^2 is complex real ext-real Element of REAL
(Re f) * (Re f) is complex real ext-real set
Im f is complex real ext-real Element of REAL
(Im f) ^2 is complex real ext-real Element of REAL
(Im f) * (Im f) is complex real ext-real set
((Re f) ^2) + ((Im f) ^2) is complex real ext-real Element of REAL
sqrt (((Re f) ^2) + ((Im f) ^2)) is complex real ext-real Element of REAL
abs (Re f) is complex real ext-real Element of REAL
Re (Re f) is complex real ext-real Element of REAL
(Re (Re f)) ^2 is complex real ext-real Element of REAL
(Re (Re f)) * (Re (Re f)) is complex real ext-real set
Im (Re f) is complex real ext-real Element of REAL
(Im (Re f)) ^2 is complex real ext-real Element of REAL
(Im (Re f)) * (Im (Re f)) is complex real ext-real set
((Re (Re f)) ^2) + ((Im (Re f)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Re f)) ^2) + ((Im (Re f)) ^2)) is complex real ext-real Element of REAL
V is complex Element of the carrier of F_Complex
Re V is complex real ext-real Element of REAL
V *' is complex Element of the carrier of F_Complex
Im V is complex real ext-real Element of REAL
(Im V) * <i> is complex set
(Re V) - ((Im V) * <i>) is complex set
Re (V *') is complex real ext-real Element of REAL
(Re V) + (Re (V *')) is complex real ext-real Element of REAL
2 * (Re V) is complex real ext-real Element of REAL
(Re V) + (Re V) is complex real ext-real Element of REAL
V is non empty VectSpStr over F_Complex
the carrier of V is non empty set
[: the carrier of V, the carrier of F_Complex:] is set
bool [: the carrier of V, the carrier of F_Complex:] is set
V is non empty VectSpStr over F_Complex
0Functional V is V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like constant V30( the carrier of V, the carrier of F_Complex) additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of F_Complex:]
the carrier of V is non empty set
[: the carrier of V, the carrier of F_Complex:] is set
bool [: the carrier of V, the carrier of F_Complex:] is set
[#] V is non empty non proper Element of bool the carrier of V
bool the carrier of V is set
K402( the carrier of F_Complex,([#] V),(0. F_Complex)) is V16() V19( [#] V) V20( the carrier of F_Complex) Function-like V30( [#] V, the carrier of F_Complex) Element of bool [:([#] V), the carrier of F_Complex:]
[:([#] V), the carrier of F_Complex:] is set
bool [:([#] V), the carrier of F_Complex:] is set
f is Element of the carrier of V
(0Functional V) . f is complex Element of the carrier of F_Complex
vq is complex Element of the carrier of F_Complex
vq * f is Element of the carrier of V
the lmult of V is V16() V19([: the carrier of F_Complex, the carrier of V:]) V20( the carrier of V) Function-like V30([: the carrier of F_Complex, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F_Complex, the carrier of V:], the carrier of V:]
[: the carrier of F_Complex, the carrier of V:] is set
[:[: the carrier of F_Complex, the carrier of V:], the carrier of V:] is set
bool [:[: the carrier of F_Complex, the carrier of V:], the carrier of V:] is set
the lmult of V . (vq,f) is Element of the carrier of V
[vq,f] is set
{vq,f} is non empty set
{vq} is non empty V175() set
{{vq,f},{vq}} is non empty set
the lmult of V . [vq,f] is set
(0Functional V) . (vq * f) is complex Element of the carrier of F_Complex
vq *' is complex Element of the carrier of F_Complex
Re vq is complex real ext-real Element of REAL
Im vq is complex real ext-real Element of REAL
(Im vq) * <i> is complex set
(Re vq) - ((Im vq) * <i>) is complex set
(vq *') * ((0Functional V) . f) is complex Element of the carrier of F_Complex
the multF of F_Complex . ((vq *'),((0Functional V) . f)) is complex Element of the carrier of F_Complex
[(vq *'),((0Functional V) . f)] is set
{(vq *'),((0Functional V) . f)} is non empty V175() set
{(vq *')} is non empty V175() set
{{(vq *'),((0Functional V) . f)},{(vq *')}} is non empty set
the multF of F_Complex . [(vq *'),((0Functional V) . f)] is set
K137((vq *'),((0Functional V) . f)) is complex Element of COMPLEX
V is non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex
the carrier of V is non empty set
[: the carrier of V, the carrier of F_Complex:] is set
bool [: the carrier of V, the carrier of F_Complex:] is set
f is V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) Element of bool [: the carrier of V, the carrier of F_Complex:]
0. V is zero Element of the carrier of V
f . (0. V) is complex Element of the carrier of F_Complex
(0. F_Complex) * (0. V) is Element of the carrier of V
the lmult of V is V16() V19([: the carrier of F_Complex, the carrier of V:]) V20( the carrier of V) Function-like V30([: the carrier of F_Complex, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F_Complex, the carrier of V:], the carrier of V:]
[: the carrier of F_Complex, the carrier of V:] is set
[:[: the carrier of F_Complex, the carrier of V:], the carrier of V:] is set
bool [:[: the carrier of F_Complex, the carrier of V:], the carrier of V:] is set
the lmult of V . ((0. F_Complex),(0. V)) is Element of the carrier of V
[(0. F_Complex),(0. V)] is set
{(0. F_Complex),(0. V)} is non empty set
{(0. F_Complex)} is non empty V175() set
{{(0. F_Complex),(0. V)},{(0. F_Complex)}} is non empty set
the lmult of V . [(0. F_Complex),(0. V)] is set
f . ((0. F_Complex) * (0. V)) is complex Element of the carrier of F_Complex
((0. F_Complex) *') * (f . (0. V)) is complex Element of the carrier of F_Complex
the multF of F_Complex . (((0. F_Complex) *'),(f . (0. V))) is complex Element of the carrier of F_Complex
[((0. F_Complex) *'),(f . (0. V))] is set
{((0. F_Complex) *'),(f . (0. V))} is non empty V175() set
{((0. F_Complex) *')} is non empty V175() set
{{((0. F_Complex) *'),(f . (0. V))},{((0. F_Complex) *')}} is non empty set
the multF of F_Complex . [((0. F_Complex) *'),(f . (0. V))] is set
K137(((0. F_Complex) *'),(f . (0. V))) is complex Element of COMPLEX
V is non empty VectSpStr over F_Complex
the carrier of V is non empty set
[: the carrier of V, the carrier of F_Complex:] is set
bool [: the carrier of V, the carrier of F_Complex:] is set
0Functional V is V16() V19( the carrier of V) V20( the carrier of F_Complex) V20( the carrier of F_Complex) Function-like constant V30( the carrier of V, the carrier of F_Complex) V30( the carrier of V, the carrier of F_Complex) additive homogeneous 0-preserving (V) Element of bool [: the carrier of V, the carrier of F_Complex:]
[#] V is non empty non proper Element of bool the carrier of V
bool the carrier of V is set
K402( the carrier of F_Complex,([#] V),(0. F_Complex)) is V16() V19( [#] V) V20( the carrier of F_Complex) Function-like V30( [#] V, the carrier of F_Complex) Element of bool [:([#] V), the carrier of F_Complex:]
[:([#] V), the carrier of F_Complex:] is set
bool [:([#] V), the carrier of F_Complex:] is set
V is non empty VectSpStr over F_Complex
the carrier of V is non empty set
[: the carrier of V, the carrier of F_Complex:] is set
bool [: the carrier of V, the carrier of F_Complex:] is set
f is V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) (V) Element of bool [: the carrier of V, the carrier of F_Complex:]
vq is V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) (V) Element of bool [: the carrier of V, the carrier of F_Complex:]
f + vq is V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) Element of bool [: the carrier of V, the carrier of F_Complex:]
vr is Element of the carrier of V
(f + vq) . vr is complex Element of the carrier of F_Complex
qh is complex Element of the carrier of F_Complex
qh * vr is Element of the carrier of V
the lmult of V is V16() V19([: the carrier of F_Complex, the carrier of V:]) V20( the carrier of V) Function-like V30([: the carrier of F_Complex, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F_Complex, the carrier of V:], the carrier of V:]
[: the carrier of F_Complex, the carrier of V:] is set
[:[: the carrier of F_Complex, the carrier of V:], the carrier of V:] is set
bool [:[: the carrier of F_Complex, the carrier of V:], the carrier of V:] is set
the lmult of V . (qh,vr) is Element of the carrier of V
[qh,vr] is set
{qh,vr} is non empty set
{qh} is non empty V175() set
{{qh,vr},{qh}} is non empty set
the lmult of V . [qh,vr] is set
(f + vq) . (qh * vr) is complex Element of the carrier of F_Complex
qh *' is complex Element of the carrier of F_Complex
Re qh is complex real ext-real Element of REAL
Im qh is complex real ext-real Element of REAL
(Im qh) * <i> is complex set
(Re qh) - ((Im qh) * <i>) is complex set
(qh *') * ((f + vq) . vr) is complex Element of the carrier of F_Complex
the multF of F_Complex . ((qh *'),((f + vq) . vr)) is complex Element of the carrier of F_Complex
[(qh *'),((f + vq) . vr)] is set
{(qh *'),((f + vq) . vr)} is non empty V175() set
{(qh *')} is non empty V175() set
{{(qh *'),((f + vq) . vr)},{(qh *')}} is non empty set
the multF of F_Complex . [(qh *'),((f + vq) . vr)] is set
K137((qh *'),((f + vq) . vr)) is complex Element of COMPLEX
f . (qh * vr) is complex Element of the carrier of F_Complex
vq . (qh * vr) is complex Element of the carrier of F_Complex
(f . (qh * vr)) + (vq . (qh * vr)) is complex Element of the carrier of F_Complex
the addF of F_Complex is V16() V19([: the carrier of F_Complex, the carrier of F_Complex:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
the addF of F_Complex . ((f . (qh * vr)),(vq . (qh * vr))) is complex Element of the carrier of F_Complex
[(f . (qh * vr)),(vq . (qh * vr))] is set
{(f . (qh * vr)),(vq . (qh * vr))} is non empty V175() set
{(f . (qh * vr))} is non empty V175() set
{{(f . (qh * vr)),(vq . (qh * vr))},{(f . (qh * vr))}} is non empty set
the addF of F_Complex . [(f . (qh * vr)),(vq . (qh * vr))] is set
K135((f . (qh * vr)),(vq . (qh * vr))) is complex Element of COMPLEX
f . vr is complex Element of the carrier of F_Complex
(qh *') * (f . vr) is complex Element of the carrier of F_Complex
the multF of F_Complex . ((qh *'),(f . vr)) is complex Element of the carrier of F_Complex
[(qh *'),(f . vr)] is set
{(qh *'),(f . vr)} is non empty V175() set
{{(qh *'),(f . vr)},{(qh *')}} is non empty set
the multF of F_Complex . [(qh *'),(f . vr)] is set
K137((qh *'),(f . vr)) is complex Element of COMPLEX
((qh *') * (f . vr)) + (vq . (qh * vr)) is complex Element of the carrier of F_Complex
the addF of F_Complex . (((qh *') * (f . vr)),(vq . (qh * vr))) is complex Element of the carrier of F_Complex
[((qh *') * (f . vr)),(vq . (qh * vr))] is set
{((qh *') * (f . vr)),(vq . (qh * vr))} is non empty V175() set
{((qh *') * (f . vr))} is non empty V175() set
{{((qh *') * (f . vr)),(vq . (qh * vr))},{((qh *') * (f . vr))}} is non empty set
the addF of F_Complex . [((qh *') * (f . vr)),(vq . (qh * vr))] is set
K135(((qh *') * (f . vr)),(vq . (qh * vr))) is complex Element of COMPLEX
vq . vr is complex Element of the carrier of F_Complex
(qh *') * (vq . vr) is complex Element of the carrier of F_Complex
the multF of F_Complex . ((qh *'),(vq . vr)) is complex Element of the carrier of F_Complex
[(qh *'),(vq . vr)] is set
{(qh *'),(vq . vr)} is non empty V175() set
{{(qh *'),(vq . vr)},{(qh *')}} is non empty set
the multF of F_Complex . [(qh *'),(vq . vr)] is set
K137((qh *'),(vq . vr)) is complex Element of COMPLEX
((qh *') * (f . vr)) + ((qh *') * (vq . vr)) is complex Element of the carrier of F_Complex
the addF of F_Complex . (((qh *') * (f . vr)),((qh *') * (vq . vr))) is complex Element of the carrier of F_Complex
[((qh *') * (f . vr)),((qh *') * (vq . vr))] is set
{((qh *') * (f . vr)),((qh *') * (vq . vr))} is non empty V175() set
{{((qh *') * (f . vr)),((qh *') * (vq . vr))},{((qh *') * (f . vr))}} is non empty set
the addF of F_Complex . [((qh *') * (f . vr)),((qh *') * (vq . vr))] is set
K135(((qh *') * (f . vr)),((qh *') * (vq . vr))) is complex Element of COMPLEX
(f . vr) + (vq . vr) is complex Element of the carrier of F_Complex
the addF of F_Complex . ((f . vr),(vq . vr)) is complex Element of the carrier of F_Complex
[(f . vr),(vq . vr)] is set
{(f . vr),(vq . vr)} is non empty V175() set
{(f . vr)} is non empty V175() set
{{(f . vr),(vq . vr)},{(f . vr)}} is non empty set
the addF of F_Complex . [(f . vr),(vq . vr)] is set
K135((f . vr),(vq . vr)) is complex Element of COMPLEX
(qh *') * ((f . vr) + (vq . vr)) is complex Element of the carrier of F_Complex
the multF of F_Complex . ((qh *'),((f . vr) + (vq . vr))) is complex Element of the carrier of F_Complex
[(qh *'),((f . vr) + (vq . vr))] is set
{(qh *'),((f . vr) + (vq . vr))} is non empty V175() set
{{(qh *'),((f . vr) + (vq . vr))},{(qh *')}} is non empty set
the multF of F_Complex . [(qh *'),((f . vr) + (vq . vr))] is set
K137((qh *'),((f . vr) + (vq . vr))) is complex Element of COMPLEX
V is non empty VectSpStr over F_Complex
the carrier of V is non empty set
[: the carrier of V, the carrier of F_Complex:] is set
bool [: the carrier of V, the carrier of F_Complex:] is set
f is V16() V19( the carrier of V) V20( the carrier of F_Complex) Function-like V30( the carrier of V, the carrier of F_Complex) (V) Element of bool [: the carrier of V, the carrier of F_Complex:]