:: VECTMETR semantic presentation

REAL is non empty V34() V64() V65() V66() V70() set
NAT is V64() V65() V66() V67() V68() V69() V70() Element of bool REAL
bool REAL is non empty set
BOOLEAN is non empty set
0 is empty ordinal natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of NAT
RAT is non empty V34() V64() V65() V66() V67() V70() set
the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set
1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
{0,1} is non empty V64() V65() V66() V67() V68() V69() set
COMPLEX is non empty V34() V64() V70() set
NAT is V64() V65() V66() V67() V68() V69() V70() set
bool NAT is non empty set
bool NAT is non empty set
K218(NAT) is V49() set
INT is non empty V34() V64() V65() V66() V67() V68() V70() set
[:NAT,REAL:] is Relation-like V53() V54() V55() set
bool [:NAT,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like V53() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like V53() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty Relation-like V53() V54() V55() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty Relation-like RAT -valued V53() V54() V55() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued V53() V54() V55() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:[:NAT,NAT:],NAT:] is non empty set
[:1,1:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
[:2,2:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
[:[:2,2:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:2,2:],REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V200() L15()
the carrier of (TOP-REAL 2) is non empty set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set
3 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg 1 is non empty V34() V41(1) V64() V65() V66() V67() V68() V69() Element of bool NAT
{1} is non empty V64() V65() V66() V67() V68() V69() set
Seg 2 is non empty V34() V41(2) V64() V65() V66() V67() V68() V69() Element of bool NAT
{1,2} is non empty V64() V65() V66() V67() V68() V69() set
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
FALSE is boolean Element of BOOLEAN
<*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' <*FALSE*> is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
TRUE is boolean Element of BOOLEAN
<*TRUE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
{0,1} is non empty V64() V65() V66() V67() V68() V69() Element of bool NAT
{0,1} * is non empty functional FinSequence-membered FinSequenceSet of {0,1}
<*0*> is non empty Relation-like NAT -defined NAT -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
<*1*> is non empty Relation-like NAT -defined NAT -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
n is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of n is non empty set
S is Element of the carrier of n
X is Element of the carrier of n
dist (S,X) is V11() real ext-real Element of REAL
[: the carrier of n, the carrier of n:] is non empty Relation-like set
x is Element of [: the carrier of n, the carrier of n:]
y is set
z is set
[y,z] is V26() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
x1 is Element of the carrier of n
1 / 2 is V11() real ext-real non negative Element of REAL
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
(1 / 2) * (dist (x1,y1)) is V11() real ext-real Element of REAL
1 - (1 / 2) is V11() real ext-real Element of REAL
(1 - (1 / 2)) * (dist (x1,y1)) is V11() real ext-real Element of REAL
z1 is Element of the carrier of n
dist (x1,z1) is V11() real ext-real Element of REAL
dist (z1,y1) is V11() real ext-real Element of REAL
[x1,z1] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,z1} is non empty set
{x1} is non empty set
{{x1,z1},{x1}} is non empty set
f is V26() Element of [: the carrier of n, the carrier of n:]
[z1,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{z1,y1} is non empty set
{z1} is non empty set
{{z1,y1},{z1}} is non empty set
f2 is V26() Element of [: the carrier of n, the carrier of n:]
f3 is Element of the carrier of n
g is Element of the carrier of n
[f3,g] is V26() Element of [: the carrier of n, the carrier of n:]
{f3,g} is non empty set
{f3} is non empty set
{{f3,g},{f3}} is non empty set
dist (f3,g) is V11() real ext-real Element of REAL
[f3,z1] is V26() Element of [: the carrier of n, the carrier of n:]
{f3,z1} is non empty set
{{f3,z1},{f3}} is non empty set
[z1,g] is V26() Element of [: the carrier of n, the carrier of n:]
{z1,g} is non empty set
{{z1,g},{z1}} is non empty set
dist (f3,z1) is V11() real ext-real Element of REAL
2 * (dist (f3,z1)) is V11() real ext-real Element of REAL
dist (z1,g) is V11() real ext-real Element of REAL
2 * (dist (z1,g)) is V11() real ext-real Element of REAL
{0,1} is non empty V64() V65() V66() V67() V68() V69() Element of bool REAL
{0,1} * is non empty functional FinSequence-membered FinSequenceSet of {0,1}
[S,X] is V26() Element of [: the carrier of n, the carrier of n:]
{S,X} is non empty set
{S} is non empty set
{{S,X},{S}} is non empty set
<*0*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
<*1*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
x is Relation-like [: the carrier of n, the carrier of n:] -valued Function-like DecoratedTree-like binary set
proj1 x is non empty Tree-like set
x . {} is set
z is V11() real ext-real Element of REAL
(dist (S,X)) / z is V11() real ext-real Element of REAL
log (2,1) is V11() real ext-real Element of REAL
log (2,((dist (S,X)) / z)) is V11() real ext-real Element of REAL
[\(log (2,((dist (S,X)) / z)))/] is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
y1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power y1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
z1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(dist (S,X)) / z1 is V11() real ext-real Element of REAL
y is non empty Tree-like finite-order binary full set
FinSeqLevel (y1,y) is Relation-like NAT -defined y -level y1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level y1
y -level y1 is V34() Level of y
f2 is Relation-like NAT -defined proj1 x -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of proj1 x
f3 is Relation-like NAT -defined [: the carrier of n, the carrier of n:] -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of [: the carrier of n, the carrier of n:]
len f3 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
dom f3 is V64() V65() V66() V67() V68() V69() Element of bool NAT
Seg z1 is non empty V34() V41(z1) V64() V65() V66() V67() V68() V69() Element of bool NAT
g is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
0* g is Relation-like NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL g
REAL g is non empty functional FinSequence-membered FinSequenceSet of REAL
g -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = g } is set
g |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of g -tuples_on REAL
Seg g is V34() V41(g) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg g),0) is Relation-like Seg g -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg g),{0}:]
{0} is non empty functional V64() V65() V66() V67() V68() V69() set
[:(Seg g),{0}:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg g),{0}:] is non empty set
x . (0* g) is set
(x . (0* g)) `1 is set
g + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
0* (g + 1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL (g + 1)
REAL (g + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(g + 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b<sub>1</sub> = g + 1 } is set
(g + 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of (g + 1) -tuples_on REAL
Seg (g + 1) is non empty V34() V41(g + 1) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg (g + 1)),0) is non empty Relation-like Seg (g + 1) -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg (g + 1)),{0}:]
[:(Seg (g + 1)),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg (g + 1)),{0}:] is non empty set
x . (0* (g + 1)) is set
(x . (0* (g + 1))) `1 is set
g2 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . g2 is Element of [: the carrier of n, the carrier of n:]
g3 is set
a is set
[g3,a] is V26() set
{g3,a} is non empty set
{g3} is non empty set
{{g3,a},{g3}} is non empty set
g2 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (g2 ^ <*0*>) is set
c is Element of the carrier of n
g2 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (g2 ^ <*1*>) is set
c1 is Element of the carrier of n
dist (c,c1) is V11() real ext-real Element of REAL
(x . (g2 ^ <*0*>)) `1 is set
j is Element of the carrier of n
[c,j] is V26() Element of [: the carrier of n, the carrier of n:]
{c,j} is non empty set
{c} is non empty set
{{c,j},{c}} is non empty set
[j,c1] is V26() Element of [: the carrier of n, the carrier of n:]
{j,c1} is non empty set
{j} is non empty set
{{j,c1},{j}} is non empty set
dist (c,j) is V11() real ext-real Element of REAL
2 * (dist (c,j)) is V11() real ext-real Element of REAL
dist (j,c1) is V11() real ext-real Element of REAL
2 * (dist (j,c1)) is V11() real ext-real Element of REAL
0* 0 is Relation-like NAT -defined REAL -valued Function-like V34() V41( 0 ) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL 0
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b<sub>1</sub> = 0 } is set
0 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41( 0 ) FinSequence-like FinSubsequence-like V53() V54() V55() Element of 0 -tuples_on REAL
Seg 0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of bool NAT
K153((Seg 0),0) is empty Relation-like non-empty empty-yielding Seg 0 -defined RAT -valued INT -valued {0} -valued Function-like one-to-one constant functional total quasi_total V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of bool [:(Seg 0),{0}:]
{0} is non empty functional V64() V65() V66() V67() V68() V69() set
[:(Seg 0),{0}:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg 0),{0}:] is non empty set
x . (0* 0) is set
(x . (0* 0)) `1 is set
0 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
len (FinSeqLevel (y1,y)) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g is non empty ordinal natural V11() real integer ext-real positive non negative set
0* g is Relation-like NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL g
REAL g is non empty functional FinSequence-membered FinSequenceSet of REAL
g -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = g } is set
g |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like V53() V54() V55() Element of g -tuples_on REAL
Seg g is non empty V34() V41(g) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg g),0) is non empty Relation-like Seg g -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg g),{0}:]
[:(Seg g),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg g),{0}:] is non empty set
g + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
0* (g + 1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL (g + 1)
REAL (g + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(g + 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = g + 1 } is set
(g + 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of (g + 1) -tuples_on REAL
Seg (g + 1) is non empty V34() V41(g + 1) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg (g + 1)),0) is non empty Relation-like Seg (g + 1) -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg (g + 1)),{0}:]
[:(Seg (g + 1)),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg (g + 1)),{0}:] is non empty set
g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' g2) is set
(x . ('not' g2)) `2 is set
g -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b<sub>1</sub> = g } is set
g3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like Element of g -tuples_on BOOLEAN
a is boolean Element of BOOLEAN
<*a*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
g3 ^ <*a*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g + 1) V41(K371(g,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K371(g,1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(0* g) ^ <*0*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(g + 1) V41(K371(g,1)) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
'not' g3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(g) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' g3) is set
(x . ('not' g3)) `2 is set
len g3 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g3) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 . ((len g3) + 1) is set
((g + 1) |-> 0) . (g + 1) is empty V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set
'not' a is boolean Element of BOOLEAN
1 - a is set
('not' g3) ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() V41(g + 1) FinSequence-like FinSubsequence-like set
c is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . c is Element of [: the carrier of n, the carrier of n:]
c1 is set
j is set
[c1,j] is V26() set
{c1,j} is non empty set
{c1} is non empty set
{{c1,j},{c1}} is non empty set
c ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c ^ <*0*>) is set
FSL1j is Element of the carrier of n
c ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c ^ <*1*>) is set
DF1 is Element of the carrier of n
dist (FSL1j,DF1) is V11() real ext-real Element of REAL
DF2 is Element of the carrier of n
[FSL1j,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{FSL1j,DF2} is non empty set
{FSL1j} is non empty set
{{FSL1j,DF2},{FSL1j}} is non empty set
[DF2,DF1] is V26() Element of [: the carrier of n, the carrier of n:]
{DF2,DF1} is non empty set
{DF2} is non empty set
{{DF2,DF1},{DF2}} is non empty set
dist (FSL1j,DF2) is V11() real ext-real Element of REAL
2 * (dist (FSL1j,DF2)) is V11() real ext-real Element of REAL
dist (DF2,DF1) is V11() real ext-real Element of REAL
2 * (dist (DF2,DF1)) is V11() real ext-real Element of REAL
0* 1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL 1
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of 1 -tuples_on REAL
K153((Seg 1),0) is non empty Relation-like Seg 1 -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg 1),{0}:]
[:(Seg 1),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg 1),{0}:] is non empty set
<*> {0,1} is empty Relation-like non-empty empty-yielding NAT -defined {0,1} -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain FinSequence of {0,1}
g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' g2 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' g2) is set
(x . ('not' g2)) `2 is set
g is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
g ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (g ^ <*0*>) is set
g ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (g ^ <*1*>) is set
(x . (g ^ <*1*>)) `2 is set
g3 is Element of the carrier of n
[S,g3] is V26() Element of [: the carrier of n, the carrier of n:]
{S,g3} is non empty set
{{S,g3},{S}} is non empty set
[g3,X] is V26() Element of [: the carrier of n, the carrier of n:]
{g3,X} is non empty set
{g3} is non empty set
{{g3,X},{g3}} is non empty set
dist (S,g3) is V11() real ext-real Element of REAL
2 * (dist (S,g3)) is V11() real ext-real Element of REAL
dist (g3,X) is V11() real ext-real Element of REAL
2 * (dist (g3,X)) is V11() real ext-real Element of REAL
g is Relation-like NAT -defined the carrier of n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len g is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
dom g is V64() V65() V66() V67() V68() V69() Element of bool NAT
<*X*> is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
g ^ <*X*> is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
g2 is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
g2 /. 1 is Element of the carrier of n
len g2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (len g2) is Element of the carrier of n
(len g2) - 1 is V11() real integer ext-real Element of REAL
len <*X*> is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g) + (len <*X*>) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
z1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 . 1 is set
g . 1 is set
f3 /. 1 is Element of [: the carrier of n, the carrier of n:]
(f3 /. 1) `1 is Element of the carrier of n
f3 . 1 is set
(f3 . 1) `1 is set
f2 /. 1 is Element of proj1 x
x . (f2 /. 1) is Element of [: the carrier of n, the carrier of n:]
(x . (f2 /. 1)) `1 is Element of the carrier of n
(FinSeqLevel (y1,y)) . 1 is set
x . ((FinSeqLevel (y1,y)) . 1) is set
(x . ((FinSeqLevel (y1,y)) . 1)) `1 is set
0* y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL y1
REAL y1 is non empty functional FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = y1 } is set
y1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like V53() V54() V55() Element of y1 -tuples_on REAL
Seg y1 is non empty V34() V41(y1) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg y1),0) is non empty Relation-like Seg y1 -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg y1),{0}:]
[:(Seg y1),{0}:] is non empty Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg y1),{0}:] is non empty set
x . (0* y1) is set
(x . (0* y1)) `1 is set
Seg (len g2) is V34() V41( len g2) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom g2 is non empty V64() V65() V66() V67() V68() V69() Element of bool NAT
(g ^ <*X*>) . ((len g) + 1) is set
y1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b<sub>1</sub> = y1 } is set
g3 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
c is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. c is Element of the carrier of n
c + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (c + 1) is Element of the carrier of n
dist ((g2 /. c),(g2 /. (c + 1))) is V11() real ext-real Element of REAL
len f2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(len g2) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(c + 1) - 1 is V11() real integer ext-real Element of REAL
(2 to_power y1) - 1 is V11() real integer ext-real Element of REAL
c1 is non empty ordinal natural V11() real integer ext-real positive non negative set
2 to_power c1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) - 1 is V11() real integer ext-real Element of REAL
FinSeqLevel (c1,y) is Relation-like NAT -defined y -level c1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of y -level c1
y -level c1 is Level of y
c1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power (c1 + 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power (c1 + 1)) - 1 is V11() real integer ext-real Element of REAL
FinSeqLevel ((c1 + 1),y) is Relation-like NAT -defined y -level (c1 + 1) -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level (c1 + 1)
y -level (c1 + 1) is V34() Level of y
DF1 is ordinal natural V11() real integer ext-real non negative set
DF1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . (DF1 + 1) is set
x . ((FinSeqLevel ((c1 + 1),y)) . (DF1 + 1)) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . (DF1 + 1))) `1 is set
(FinSeqLevel ((c1 + 1),y)) . DF1 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF1) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF1)) `2 is set
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power (c1 + 1)) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 to_power (c1 + 1)) -' 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 to_power (c1 + 1)) - 1) + 1 is V11() real integer ext-real Element of REAL
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * (2 to_power 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 + 1) + 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg (2 to_power c1) is V34() V41(2 to_power c1) V64() V65() V66() V67() V68() V69() Element of bool NAT
j is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel (j,y) is Relation-like NAT -defined y -level j -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level j
y -level j is V34() Level of y
dom (FinSeqLevel (j,y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
(FinSeqLevel (c1,y)) . (((DF1 + 1) + 1) div 2) is set
FSL1j is non empty set
(FinSeqLevel (j,y)) . (((DF1 + 1) + 1) div 2) is set
c1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b<sub>1</sub> = c1 } is set
b is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FSLlprim is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
FSLlprim is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . FSLlprim is Element of [: the carrier of n, the carrier of n:]
Fj is set
FSLl1 is set
[Fj,FSLl1] is V26() set
{Fj,FSLl1} is non empty set
{Fj} is non empty set
{{Fj,FSLl1},{Fj}} is non empty set
(FinSeqLevel (c1,y)) . ((DF1 + 1) div 2) is set
(FinSeqLevel (j,y)) . ((DF1 + 1) div 2) is set
FSLl is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
d is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
DF1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . DF1 is Element of [: the carrier of n, the carrier of n:]
DF2 is set
NFSLl is set
[DF2,NFSLl] is V26() set
{DF2,NFSLl} is non empty set
{DF2} is non empty set
{{DF2,NFSLl},{DF2}} is non empty set
DF1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (DF1 ^ <*0*>) is set
x1 is Element of the carrier of n
DF1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (DF1 ^ <*1*>) is set
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
b is Element of the carrier of n
[x1,b] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,b} is non empty set
{x1} is non empty set
{{x1,b},{x1}} is non empty set
[b,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{b,y1} is non empty set
{b} is non empty set
{{b,y1},{b}} is non empty set
dist (x1,b) is V11() real ext-real Element of REAL
2 * (dist (x1,b)) is V11() real ext-real Element of REAL
dist (b,y1) is V11() real ext-real Element of REAL
2 * (dist (b,y1)) is V11() real ext-real Element of REAL
FSLlprim ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*0*>) is set
x1 is Element of the carrier of n
FSLlprim ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*1*>) is set
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
d9 is Element of the carrier of n
[x1,d9] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,d9} is non empty set
{x1} is non empty set
{{x1,d9},{x1}} is non empty set
[d9,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{d9,y1} is non empty set
{d9} is non empty set
{{d9,y1},{d9}} is non empty set
dist (x1,d9) is V11() real ext-real Element of REAL
2 * (dist (x1,d9)) is V11() real ext-real Element of REAL
dist (d9,y1) is V11() real ext-real Element of REAL
2 * (dist (d9,y1)) is V11() real ext-real Element of REAL
(DF1 + 1) - 1 is V11() real integer ext-real Element of REAL
(DF1 + 1) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 * 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 * 1) + DF1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 * 1) + DF1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>) is set
(x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>)) `1 is set
FSLlprim ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*1*>) is set
(x . (FSLlprim ^ <*1*>)) `1 is set
d ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (d ^ <*0*>) is set
(x . (d ^ <*0*>)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF2 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF2 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
d ^ <*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (d ^ <*((DF2 + 1) mod 2)*>) is set
(x . (d ^ <*((DF2 + 1) mod 2)*>)) `2 is set
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF1 mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 -' 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 * 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 -' 1) + (2 * 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 -' 1) + (2 * 1)) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 -' 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 -' 1) + 1) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((DF1 -' 1) + 1) + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF1 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
1 + DF1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
1 + (1 + DF1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(1 + 1) + (DF1 -' 1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 - 1 is V11() real integer ext-real Element of REAL
(1 + 1) + (DF1 - 1) is V11() real integer ext-real Element of REAL
(1 + 1) + DF1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((1 + 1) + DF1) - 1 is V11() real integer ext-real Element of REAL
((1 + 1) + DF1) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((1 + 1) + DF1) -' 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((1 + 1) + DF1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 * (((DF1 + 1) + 1) div 2) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 * (((DF1 + 1) + 1) div 2)) + 0 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((DF1 + 1) + 1) -' 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((DF1 + 1) + 1) -' 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(((DF1 + 1) + 1) div 2) - 1 is V11() real integer ext-real Element of REAL
((DF1 + 1) div 2) + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x . ((FinSeqLevel (c1,y)) . (((DF1 + 1) + 1) div 2)) is set
(x . ((FinSeqLevel (c1,y)) . (((DF1 + 1) + 1) div 2))) `1 is set
x . ((FinSeqLevel (c1,y)) . ((DF1 + 1) div 2)) is set
(x . ((FinSeqLevel (c1,y)) . ((DF1 + 1) div 2))) `2 is set
(2 * 1) + DF1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
((2 * 1) + DF1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>) is set
(x . (FSLlprim ^ <*(((2 * 1) + DF1) mod 2)*>)) `1 is set
FSLlprim ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (FSLlprim ^ <*0*>) is set
(x . (FSLlprim ^ <*0*>)) `1 is set
d ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
x . (d ^ <*1*>) is set
(x . (d ^ <*1*>)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power 1) - 1 is V11() real integer ext-real Element of REAL
FinSeqLevel (1,y) is Relation-like NAT -defined y -level 1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level 1
y -level 1 is V34() Level of y
<*> {0,1} is empty Relation-like non-empty empty-yielding NAT -defined {0,1} -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain FinSequence of {0,1}
j is ordinal natural V11() real integer ext-real non negative set
j + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel (1,y)) . (j + 1) is set
x . ((FinSeqLevel (1,y)) . (j + 1)) is set
(x . ((FinSeqLevel (1,y)) . (j + 1))) `1 is set
(FinSeqLevel (1,y)) . j is set
x . ((FinSeqLevel (1,y)) . j) is set
(x . ((FinSeqLevel (1,y)) . j)) `2 is set
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(1 + 1) - 1 is V11() real integer ext-real Element of REAL
c1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
c1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*0*>) is set
c1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*1*>) is set
FSL1j is Element of the carrier of n
[S,FSL1j] is V26() Element of [: the carrier of n, the carrier of n:]
{S,FSL1j} is non empty set
{{S,FSL1j},{S}} is non empty set
[FSL1j,X] is V26() Element of [: the carrier of n, the carrier of n:]
{FSL1j,X} is non empty set
{FSL1j} is non empty set
{{FSL1j,X},{FSL1j}} is non empty set
dist (S,FSL1j) is V11() real ext-real Element of REAL
2 * (dist (S,FSL1j)) is V11() real ext-real Element of REAL
dist (FSL1j,X) is V11() real ext-real Element of REAL
2 * (dist (FSL1j,X)) is V11() real ext-real Element of REAL
x . <*1*> is set
(x . <*1*>) `1 is set
(x . (c1 ^ <*1*>)) `1 is set
(x . (c1 ^ <*0*>)) `2 is set
x . <*0*> is set
(x . <*0*>) `2 is set
1 + c is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg (len g) is V34() V41( len g) V64() V65() V66() V67() V68() V69() Element of bool NAT
g /. (c + 1) is Element of the carrier of n
g . (c + 1) is set
f3 /. (c + 1) is Element of [: the carrier of n, the carrier of n:]
(f3 /. (c + 1)) `1 is Element of the carrier of n
f3 . (c + 1) is set
(f3 . (c + 1)) `1 is set
f2 /. (c + 1) is Element of proj1 x
x . (f2 /. (c + 1)) is Element of [: the carrier of n, the carrier of n:]
(x . (f2 /. (c + 1))) `1 is Element of the carrier of n
(FinSeqLevel (y1,y)) . (c + 1) is set
x . ((FinSeqLevel (y1,y)) . (c + 1)) is set
(x . ((FinSeqLevel (y1,y)) . (c + 1))) `1 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
a is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like Element of y1 -tuples_on BOOLEAN
'not' a is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(y1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x . ('not' a) is set
(x . ('not' a)) `2 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
(FinSeqLevel (y1,y)) . c is set
x . ((FinSeqLevel (y1,y)) . c) is set
(x . ((FinSeqLevel (y1,y)) . c)) `2 is set
c1 is non empty ordinal natural V11() real integer ext-real positive non negative set
2 to_power c1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel (c1,y) is Relation-like NAT -defined y -level c1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of y -level c1
y -level c1 is Level of y
(dist (S,X)) / (2 to_power c1) is V11() real ext-real Element of REAL
c1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power (c1 + 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel ((c1 + 1),y) is Relation-like NAT -defined y -level (c1 + 1) -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level (c1 + 1)
y -level (c1 + 1) is V34() Level of y
(dist (S,X)) / (2 to_power (c1 + 1)) is V11() real ext-real Element of REAL
DF2 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel ((c1 + 1),y)) . DF2 is set
x . ((FinSeqLevel ((c1 + 1),y)) . DF2) is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `1 is set
(x . ((FinSeqLevel ((c1 + 1),y)) . DF2)) `2 is set
DF2 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(DF2 + 1) div 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * (2 to_power 1) is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(2 to_power c1) * 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
b is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Seg (2 to_power c1) is V34() V41(2 to_power c1) V64() V65() V66() V67() V68() V69() Element of bool NAT
FSL1j is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel (FSL1j,y) is Relation-like NAT -defined y -level FSL1j -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level FSL1j
y -level FSL1j is V34() Level of y
dom (FinSeqLevel (FSL1j,y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
(FinSeqLevel (c1,y)) . ((DF2 + 1) div 2) is set
j is non empty set
(FinSeqLevel (FSL1j,y)) . ((DF2 + 1) div 2) is set
c1 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined BOOLEAN -valued Function-like V34() FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b<sub>1</sub> = c1 } is set
FSLlprim is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Seg (2 to_power (c1 + 1)) is V34() V41(2 to_power (c1 + 1)) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom (FinSeqLevel ((c1 + 1),y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
DF1 is non empty set
FSLl1 is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FSLl is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
d is boolean Element of BOOLEAN
<*d*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
FSLl ^ <*d*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1 + 1) V41(K371(c1,1)) FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
K371(c1,1) is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
DF1 is Element of the carrier of n
DF2 is Element of the carrier of n
dist (DF1,DF2) is V11() real ext-real Element of REAL
Fj is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . Fj is Element of [: the carrier of n, the carrier of n:]
[DF1,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{DF1,DF2} is non empty set
{DF1} is non empty set
{{DF1,DF2},{DF1}} is non empty set
NFSLl is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . NFSLl is Element of [: the carrier of n, the carrier of n:]
x1 is set
y1 is set
[x1,y1] is V26() set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
NFSLl ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (NFSLl ^ <*0*>) is set
x1 is Element of the carrier of n
NFSLl ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (NFSLl ^ <*1*>) is set
y1 is Element of the carrier of n
dist (x1,y1) is V11() real ext-real Element of REAL
b is Element of the carrier of n
[x1,b] is V26() Element of [: the carrier of n, the carrier of n:]
{x1,b} is non empty set
{x1} is non empty set
{{x1,b},{x1}} is non empty set
[b,y1] is V26() Element of [: the carrier of n, the carrier of n:]
{b,y1} is non empty set
{b} is non empty set
{{b,y1},{b}} is non empty set
dist (x1,b) is V11() real ext-real Element of REAL
2 * (dist (x1,b)) is V11() real ext-real Element of REAL
dist (b,y1) is V11() real ext-real Element of REAL
2 * (dist (b,y1)) is V11() real ext-real Element of REAL
FSL1j + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel ((FSL1j + 1),y) is Relation-like NAT -defined y -level (FSL1j + 1) -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level (FSL1j + 1)
y -level (FSL1j + 1) is V34() Level of y
(FinSeqLevel ((FSL1j + 1),y)) . DF2 is set
FSLlprim is Relation-like NAT -defined BOOLEAN -valued Function-like V34() V41(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on BOOLEAN
(DF2 + 1) mod 2 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
<*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1) FinSequence-like FinSubsequence-like set
FSLlprim ^ <*((DF2 + 1) mod 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(c1 + 1) FinSequence-like FinSubsequence-like set
(FinSeqLevel (c1,y)) . b is set
x . ((FinSeqLevel (c1,y)) . b) is set
(x . ((FinSeqLevel (c1,y)) . b)) `1 is set
(x . ((FinSeqLevel (c1,y)) . b)) `2 is set
2 * (dist (DF1,DF2)) is V11() real ext-real Element of REAL
((dist (S,X)) / (2 to_power c1)) / 2 is V11() real ext-real Element of REAL
(((dist (S,X)) / (2 to_power c1)) / 2) * 2 is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * 2) is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * (2 to_power 1)) is V11() real ext-real Element of REAL
2 * (dist (DF1,DF2)) is V11() real ext-real Element of REAL
((dist (S,X)) / (2 to_power c1)) / 2 is V11() real ext-real Element of REAL
(((dist (S,X)) / (2 to_power c1)) / 2) * 2 is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * 2) is V11() real ext-real Element of REAL
(dist (S,X)) / ((2 to_power c1) * (2 to_power 1)) is V11() real ext-real Element of REAL
2 to_power 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
FinSeqLevel (1,y) is Relation-like NAT -defined y -level 1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of y -level 1
y -level 1 is V34() Level of y
(dist (S,X)) / (2 to_power 1) is V11() real ext-real Element of REAL
<*> {0,1} is empty Relation-like non-empty empty-yielding NAT -defined {0,1} -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain FinSequence of {0,1}
j is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(FinSeqLevel (1,y)) . j is set
x . ((FinSeqLevel (1,y)) . j) is set
(x . ((FinSeqLevel (1,y)) . j)) `1 is set
(x . ((FinSeqLevel (1,y)) . j)) `2 is set
Seg (2 to_power 1) is V34() V41(2 to_power 1) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom (FinSeqLevel (1,y)) is V64() V65() V66() V67() V68() V69() Element of bool NAT
DF1 is Element of the carrier of n
DF2 is Element of the carrier of n
dist (DF1,DF2) is V11() real ext-real Element of REAL
c1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
c1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*0*>) is set
c1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*1*>) is set
x . <*0*> is set
FSL1j is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . FSL1j is Element of [: the carrier of n, the carrier of n:]
[DF1,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{DF1,DF2} is non empty set
{DF1} is non empty set
{{DF1,DF2},{DF1}} is non empty set
b is Element of the carrier of n
[S,b] is V26() Element of [: the carrier of n, the carrier of n:]
{S,b} is non empty set
{{S,b},{S}} is non empty set
[b,X] is V26() Element of [: the carrier of n, the carrier of n:]
{b,X} is non empty set
{b} is non empty set
{{b,X},{b}} is non empty set
dist (S,b) is V11() real ext-real Element of REAL
2 * (dist (S,b)) is V11() real ext-real Element of REAL
dist (b,X) is V11() real ext-real Element of REAL
2 * (dist (b,X)) is V11() real ext-real Element of REAL
(dist (S,X)) / 2 is V11() real ext-real Element of REAL
b is Element of the carrier of n
[S,b] is V26() Element of [: the carrier of n, the carrier of n:]
{S,b} is non empty set
{{S,b},{S}} is non empty set
[b,X] is V26() Element of [: the carrier of n, the carrier of n:]
{b,X} is non empty set
{b} is non empty set
{{b,X},{b}} is non empty set
dist (S,b) is V11() real ext-real Element of REAL
2 * (dist (S,b)) is V11() real ext-real Element of REAL
dist (b,X) is V11() real ext-real Element of REAL
2 * (dist (b,X)) is V11() real ext-real Element of REAL
c1 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
c1 ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*0*>) is set
c1 ^ <*1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
x . (c1 ^ <*1*>) is set
b is Element of the carrier of n
[S,b] is V26() Element of [: the carrier of n, the carrier of n:]
{S,b} is non empty set
{{S,b},{S}} is non empty set
[b,X] is V26() Element of [: the carrier of n, the carrier of n:]
{b,X} is non empty set
{b} is non empty set
{{b,X},{b}} is non empty set
dist (S,b) is V11() real ext-real Element of REAL
2 * (dist (S,b)) is V11() real ext-real Element of REAL
dist (b,X) is V11() real ext-real Element of REAL
2 * (dist (b,X)) is V11() real ext-real Element of REAL
x . <*1*> is set
FSL1j is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of proj1 x
x . FSL1j is Element of [: the carrier of n, the carrier of n:]
[DF1,DF2] is V26() Element of [: the carrier of n, the carrier of n:]
{DF1,DF2} is non empty set
{DF1} is non empty set
{{DF1,DF2},{DF1}} is non empty set
(dist (S,X)) / 2 is V11() real ext-real Element of REAL
(dist (S,X)) / 2 is V11() real ext-real Element of REAL
(dist (S,X)) / 2 is V11() real ext-real Element of REAL
Seg (len g) is V34() V41( len g) V64() V65() V66() V67() V68() V69() Element of bool NAT
g /. c is Element of the carrier of n
g . c is set
f3 /. c is Element of [: the carrier of n, the carrier of n:]
(f3 /. c) `1 is Element of the carrier of n
f3 . c is set
(f3 . c) `1 is set
f2 /. c is Element of proj1 x
x . (f2 /. c) is Element of [: the carrier of n, the carrier of n:]
(x . (f2 /. c)) `1 is Element of the carrier of n
(x . ((FinSeqLevel (y1,y)) . c)) `1 is set
y1 * 1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
log (2,2) is V11() real ext-real Element of REAL
y1 * (log (2,2)) is V11() real ext-real Element of REAL
log (2,(2 to_power y1)) is V11() real ext-real Element of REAL
z1 * z is V11() real ext-real Element of REAL
((dist (S,X)) / z) * z is V11() real ext-real Element of REAL
(z1 * z) / z1 is V11() real ext-real Element of REAL
z / z1 is V11() real ext-real Element of REAL
(z / z1) * z1 is V11() real ext-real Element of REAL
g3 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. g3 is Element of the carrier of n
g3 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (g3 + 1) is Element of the carrier of n
dist ((g2 /. g3),(g2 /. (g3 + 1))) is V11() real ext-real Element of REAL
g3 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len g3 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Sum g3 is V11() real ext-real Element of REAL
K381() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K219(REAL,g3,K381()) is V11() real ext-real Element of REAL
rng g3 is V64() V65() V66() Element of bool REAL
{((dist (S,X)) / z1)} is non empty V64() V65() V66() Element of bool REAL
a is set
dom g3 is V64() V65() V66() V67() V68() V69() Element of bool NAT
c is set
g3 . c is V11() real ext-real set
Seg (len g3) is V34() V41( len g3) V64() V65() V66() V67() V68() V69() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT : ( 1 <= b₁ & b₁ <= len g3 ) } is set
c1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g3 /. c1 is V11() real ext-real Element of REAL
g2 /. c1 is Element of the carrier of n
c1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (c1 + 1) is Element of the carrier of n
dist ((g2 /. c1),(g2 /. (c1 + 1))) is V11() real ext-real Element of REAL
a is set
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
g2 /. (1 + 1) is Element of the carrier of n
dist ((g2 /. 1),(g2 /. (1 + 1))) is V11() real ext-real Element of REAL
g3 /. 1 is V11() real ext-real Element of REAL
g3 . 1 is V11() real ext-real set
Seg (len g3) is V34() V41( len g3) V64() V65() V66() V67() V68() V69() Element of bool NAT
dom g3 is V64() V65() V66() V67() V68() V69() Element of bool NAT
dom g3 is V64() V65() V66() V67() V68() V69() Element of bool NAT
Seg (len g3) is V34() V41( len g3) V64() V65() V66() V67() V68() V69() Element of bool NAT
(len g3) |-> ((dist (S,X)) / z1) is Relation-like NAT -defined REAL -valued Function-like V34() V41( len g3) FinSequence-like FinSubsequence-like V53() V54() V55() Element of (len g3) -tuples_on REAL
(len g3) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = len g3 } is set
K153((Seg (len g3)),((dist (S,X)) / z1)) is Relation-like Seg (len g3) -defined {((dist (S,X)) / z1)} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() Element of bool [:(Seg (len g3)),{((dist (S,X)) / z1)}:]
{((dist (S,X)) / z1)} is non empty V64() V65() V66() set
[:(Seg (len g3)),{((dist (S,X)) / z1)}:] is Relation-like V53() V54() V55() set
bool [:(Seg (len g3)),{((dist (S,X)) / z1)}:] is non empty set
(z1 + 1) - 1 is V11() real integer ext-real Element of REAL
((z1 + 1) - 1) * ((dist (S,X)) / z1) is V11() real ext-real Element of REAL
<*S,X*> is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
x1 is non empty Relation-like NAT -defined the carrier of n -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
x1 /. 1 is Element of the carrier of n
len x1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x1 /. (len x1) is Element of the carrier of n
(len x1) - 1 is V11() real integer ext-real Element of REAL
1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(1 + 1) - 1 is V11() real integer ext-real Element of REAL
y1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x1 /. y1 is Element of the carrier of n
y1 + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
x1 /. (y1 + 1) is Element of the carrier of n
dist ((x1 /. y1),(x1 /. (y1 + 1))) is V11() real ext-real Element of REAL
y1 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len y1 is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Sum y1 is V11() real ext-real Element of REAL
K381() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K219(REAL,y1,K381()) is V11() real ext-real Element of REAL
y1 /. 1 is V11() real ext-real Element of REAL
x1 /. (1 + 1) is Element of the carrier of n
dist ((x1 /. 1),(x1 /. (1 + 1))) is V11() real ext-real Element of REAL
<*(dist (S,X))*> is non empty Relation-like NAT -defined REAL -valued Function-like V34() V41(1) FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
n is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of n is non empty set
G is Element of the carrier of n
S is Element of the carrier of n
dist (G,S) is V11() real ext-real Element of REAL
X is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
dist (G,S) is V11() real ext-real Element of REAL
y is Relation-like NAT -defined the carrier of n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
y /. 1 is Element of the carrier of n
len y is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
y /. (len y) is Element of the carrier of n
(len y) - 1 is V11() real integer ext-real Element of REAL
z is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
y /. z is Element of the carrier of n
z + 1 is non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
y /. (z + 1) is Element of the carrier of n
dist ((y /. z),(y /. (z + 1))) is V11() real ext-real Element of REAL
z is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len z is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
Sum z is V11() real ext-real Element of REAL
K381() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K219(REAL,z,K381()) is V11() real ext-real Element of REAL
(dist (G,S)) - (Sum z) is V11() real ext-real Element of REAL
abs ((dist (G,S)) - (Sum z)) is V11() real ext-real Element of REAL
(dist (G,S)) - (Sum z) is V11() real ext-real Element of REAL
abs ((dist (G,S)) - (Sum z)) is V11() real ext-real Element of REAL
{0} is non empty functional V64() V65() V66() V67() V68() V69() Element of bool REAL
n is non empty set
[:n,n:] is non empty Relation-like set
[:[:n,n:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:n,n:],REAL:] is non empty set
G is non empty Relation-like [:n,n:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[:n,n:],REAL:]
MetrStruct(# n,G #) is strict MetrStruct
S is non empty MetrStruct
the carrier of S is non empty set
X is Element of the carrier of S
x is Element of the carrier of S
dist (X,x) is V11() real ext-real Element of REAL
G . (X,x) is set
G . (x,X) is set
dist (x,X) is V11() real ext-real Element of REAL
X is Element of the carrier of S
dist (X,X) is V11() real ext-real Element of REAL
G . (X,X) is set
y is Element of the carrier of S
X is Element of the carrier of S
x is Element of the carrier of S
dist (X,y) is V11() real ext-real Element of REAL
dist (X,x) is V11() real ext-real Element of REAL
dist (x,y) is V11() real ext-real Element of REAL
(dist (X,x)) + (dist (x,y)) is V11() real ext-real Element of REAL
X is Element of the carrier of S
x is Element of the carrier of S
dist (X,x) is V11() real ext-real Element of REAL
X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
dist (x,y) is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
z * (dist (x,y)) is V11() real ext-real Element of REAL
1 - z is V11() real ext-real Element of REAL
(1 - z) * (dist (x,y)) is V11() real ext-real Element of REAL
x1 is Element of the carrier of X
dist (x,x1) is V11() real ext-real Element of REAL
dist (x1,y) is V11() real ext-real Element of REAL
dist (x1,y) is V11() real ext-real Element of REAL
G . (x1,y) is set
dist (x,x1) is V11() real ext-real Element of REAL
G . (x,x1) is set
dist (x,y) is V11() real ext-real Element of REAL
z * (dist (x,y)) is V11() real ext-real Element of REAL
(1 - z) * (dist (x,y)) is V11() real ext-real Element of REAL
n is non empty MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
n is non empty MetrStruct
the carrier of n is non empty set
id n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
id the carrier of n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of n, the carrier of n:]
proj2 (id n) is non empty set
G is Element of the carrier of n
S is Element of the carrier of n
dist (G,S) is V11() real ext-real Element of REAL
(id n) . G is Element of the carrier of n
(id n) . S is Element of the carrier of n
dist (((id n) . G),((id n) . S)) is V11() real ext-real Element of REAL
dist (((id n) . G),S) is V11() real ext-real Element of REAL
n is non empty MetrStruct
the carrier of n is non empty set
id n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto (n) Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
id the carrier of n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of n, the carrier of n:]
G is non empty MetrStruct
id G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like total quasi_total onto (G) Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is non empty Relation-like set
bool [: the carrier of G, the carrier of G:] is non empty set
id the carrier of G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of G, the carrier of G:]
n is non empty MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
id the carrier of n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of n, the carrier of n:]
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of n, the carrier of n:]
proj2 G is non empty set
S is Element of the carrier of n
X is Element of the carrier of n
dist (S,X) is V11() real ext-real Element of REAL
G . S is Element of the carrier of n
G . X is Element of the carrier of n
dist ((G . S),(G . X)) is V11() real ext-real Element of REAL
dist ((G . S),X) is V11() real ext-real Element of REAL
n is non empty MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
Funcs ( the carrier of n, the carrier of n) is non empty functional FUNCTION_DOMAIN of the carrier of n, the carrier of n
G is set
S is set
n is non empty MetrStruct
(n) is set
the carrier of n is non empty set
Funcs ( the carrier of n, the carrier of n) is non empty functional FUNCTION_DOMAIN of the carrier of n, the carrier of n
bool (Funcs ( the carrier of n, the carrier of n)) is non empty set
G is set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
n is non empty Reflexive discerning MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of n:]
S is set
dom G is non empty Element of bool the carrier of n
bool the carrier of n is non empty set
X is set
G . S is set
G . X is set
x is Element of the carrier of n
y is Element of the carrier of n
dist (x,y) is V11() real ext-real Element of REAL
G . x is Element of the carrier of n
G . y is Element of the carrier of n
dist ((G . x),(G . y)) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of n:]
n is non empty Reflexive discerning MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total onto bijective (n) Element of bool [: the carrier of n, the carrier of n:]
G " is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of n:]
proj2 G is non empty set
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is non empty set
proj2 (G ") is non empty set
S is Element of the carrier of n
X is Element of the carrier of n
dist (S,X) is V11() real ext-real Element of REAL
(G ") . S is Element of the carrier of n
(G ") . X is Element of the carrier of n
dist (((G ") . S),((G ") . X)) is V11() real ext-real Element of REAL
dom (G ") is non empty Element of bool the carrier of n
id (proj2 G) is non empty Relation-like proj2 G -defined proj2 G -valued Function-like one-to-one total quasi_total Element of bool [:(proj2 G),(proj2 G):]
[:(proj2 G),(proj2 G):] is non empty Relation-like set
bool [:(proj2 G),(proj2 G):] is non empty set
(id (proj2 G)) . X is set
G * (G ") is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of n:]
(G * (G ")) . X is Element of the carrier of n
G . ((G ") . X) is Element of the carrier of n
(id (proj2 G)) . S is set
(G * (G ")) . S is Element of the carrier of n
G . ((G ") . S) is Element of the carrier of n
n is non empty Reflexive discerning MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
S is non empty Reflexive discerning MetrStruct
the carrier of S is non empty set
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total onto bijective (n) Element of bool [: the carrier of n, the carrier of n:]
G " is non empty Relation-like the carrier of n -defined the carrier of n -defined the carrier of n -valued the carrier of n -valued Function-like one-to-one total quasi_total quasi_total onto bijective (n) Element of bool [: the carrier of n, the carrier of n:]
X is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one total quasi_total onto bijective (S) Element of bool [: the carrier of S, the carrier of S:]
X " is non empty Relation-like the carrier of S -defined the carrier of S -defined the carrier of S -valued the carrier of S -valued Function-like one-to-one total quasi_total quasi_total onto bijective (S) Element of bool [: the carrier of S, the carrier of S:]
n is non empty MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
S is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto (n) Element of bool [: the carrier of n, the carrier of n:]
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto (n) Element of bool [: the carrier of n, the carrier of n:]
G * S is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto Element of bool [: the carrier of n, the carrier of n:]
proj2 S is non empty set
dom G is non empty Element of bool the carrier of n
bool the carrier of n is non empty set
proj2 (G * S) is non empty set
proj2 G is non empty set
X is Element of the carrier of n
x is Element of the carrier of n
dist (X,x) is V11() real ext-real Element of REAL
(G * S) . X is Element of the carrier of n
(G * S) . x is Element of the carrier of n
dist (((G * S) . X),((G * S) . x)) is V11() real ext-real Element of REAL
dom S is non empty Element of bool the carrier of n
S . X is Element of the carrier of n
S . x is Element of the carrier of n
dist ((S . X),(S . x)) is V11() real ext-real Element of REAL
G . (S . X) is Element of the carrier of n
G . (S . x) is Element of the carrier of n
dist ((G . (S . X)),(G . (S . x))) is V11() real ext-real Element of REAL
dist (((G * S) . X),(G . (S . x))) is V11() real ext-real Element of REAL
X is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of n:]
n is non empty MetrStruct
the carrier of n is non empty set
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
X is non empty MetrStruct
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
S is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto (n) Element of bool [: the carrier of n, the carrier of n:]
G is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto (n) Element of bool [: the carrier of n, the carrier of n:]
G * S is non empty Relation-like the carrier of n -defined the carrier of n -defined the carrier of n -valued the carrier of n -valued Function-like total total quasi_total quasi_total onto onto (n) Element of bool [: the carrier of n, the carrier of n:]
y is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like total quasi_total onto (X) Element of bool [: the carrier of X, the carrier of X:]
x is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like total quasi_total onto (X) Element of bool [: the carrier of X, the carrier of X:]
x * y is non empty Relation-like the carrier of X -defined the carrier of X -defined the carrier of X -valued the carrier of X -valued Function-like total total quasi_total quasi_total onto onto (X) Element of bool [: the carrier of X, the carrier of X:]
n is non empty MetrStruct
(n) is functional Element of bool (Funcs ( the carrier of n, the carrier of n))
the carrier of n is non empty set
Funcs ( the carrier of n, the carrier of n) is non empty functional FUNCTION_DOMAIN of the carrier of n, the carrier of n
bool (Funcs ( the carrier of n, the carrier of n)) is non empty set
id n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like total quasi_total onto (n) Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
id the carrier of n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of n, the carrier of n:]
the non empty set is non empty set
[: the non empty set , the non empty set :] is non empty Relation-like set
[:[: the non empty set , the non empty set :],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[: the non empty set , the non empty set :],REAL:] is non empty set
the non empty Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the non empty set , the non empty set :],REAL:] is non empty Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the non empty set , the non empty set :],REAL:]
the Element of the non empty set is Element of the non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is non empty Relation-like set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the non empty Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
[:REAL, the non empty set :] is non empty Relation-like set
[:[:REAL, the non empty set :], the non empty set :] is non empty Relation-like set
bool [:[:REAL, the non empty set :], the non empty set :] is non empty set
the non empty Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :] is non empty Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :]
( the non empty set , the non empty Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the non empty set , the non empty set :],REAL:], the Element of the non empty set , the non empty Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :]) is () ()
the carrier of ( the non empty set , the non empty Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the non empty set , the non empty set :],REAL:], the Element of the non empty set , the non empty Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like total quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :]) is set
n is non empty set
[:n,n:] is non empty Relation-like set
[:[:n,n:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:n,n:],REAL:] is non empty set
[:[:n,n:],n:] is non empty Relation-like set
bool [:[:n,n:],n:] is non empty set
[:REAL,n:] is non empty Relation-like set
[:[:REAL,n:],n:] is non empty Relation-like set
bool [:[:REAL,n:],n:] is non empty set
G is non empty Relation-like [:n,n:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[:n,n:],REAL:]
S is Element of n
X is non empty Relation-like [:n,n:] -defined n -valued Function-like total quasi_total Element of bool [:[:n,n:],n:]
x is non empty Relation-like [:REAL,n:] -defined n -valued Function-like total quasi_total Element of bool [:[:REAL,n:],n:]
(n,G,S,X,x) is () ()
n is non empty ()
the carrier of n is non empty set
0. n is V108(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
G is Element of the carrier of n
dist ((0. n),G) is V11() real ext-real Element of REAL
{0} is non empty functional V64() V65() V66() V67() V68() V69() Element of bool REAL
n is non empty set
[:n,n:] is non empty Relation-like set
[:[:n,n:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:n,n:],REAL:] is non empty set
S is non empty Relation-like [:n,n:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[:n,n:],REAL:]
G is Element of n
[:[:n,n:],n:] is non empty Relation-like set
bool [:[:n,n:],n:] is non empty set
X is non empty Relation-like [:n,n:] -defined n -valued Function-like total quasi_total Element of bool [:[:n,n:],n:]
[:REAL,n:] is non empty Relation-like set
[:[:REAL,n:],n:] is non empty Relation-like set
bool [:[:REAL,n:],n:] is non empty set
x is non empty Relation-like [:REAL,n:] -defined n -valued Function-like total quasi_total Element of bool [:[:REAL,n:],n:]
(n,S,G,X,x) is non empty () ()
the carrier of (n,S,G,X,x) is non empty set
z is V11() real ext-real set
x1 is V11() real ext-real set
z + x1 is V11() real ext-real set
f is Element of the carrier of (n,S,G,X,x)
(z + x1) * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) is non empty Relation-like [:REAL, the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[:REAL, the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the Mult of (n,S,G,X,x) . ((z + x1),f) is set
z * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (z,f) is set
x1 * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (x1,f) is set
(z * f) + (x1 * f) is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . ((z * f),(x1 * f)) is Element of the carrier of (n,S,G,X,x)
y1 is V11() real ext-real Element of REAL
z1 is V11() real ext-real Element of REAL
y1 + z1 is V11() real ext-real Element of REAL
(y1 + z1) * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . ((y1 + z1),f) is set
f3 is Element of n
z is Element of the carrier of (n,S,G,X,x)
x1 is Element of the carrier of (n,S,G,X,x)
z + x1 is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . (z,x1) is Element of the carrier of (n,S,G,X,x)
x1 + z is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . (x1,z) is Element of the carrier of (n,S,G,X,x)
y1 is Element of n
z1 is Element of n
z is Element of the carrier of (n,S,G,X,x)
x1 is Element of the carrier of (n,S,G,X,x)
z + x1 is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . (z,x1) is Element of the carrier of (n,S,G,X,x)
y1 is Element of the carrier of (n,S,G,X,x)
(z + x1) + y1 is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . ((z + x1),y1) is Element of the carrier of (n,S,G,X,x)
x1 + y1 is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . (x1,y1) is Element of the carrier of (n,S,G,X,x)
z + (x1 + y1) is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . (z,(x1 + y1)) is Element of the carrier of (n,S,G,X,x)
z1 is Element of n
f is Element of n
f2 is Element of n
0. (n,S,G,X,x) is V108((n,S,G,X,x)) Element of the carrier of (n,S,G,X,x)
the ZeroF of (n,S,G,X,x) is Element of the carrier of (n,S,G,X,x)
z is Element of the carrier of (n,S,G,X,x)
z + (0. (n,S,G,X,x)) is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . (z,(0. (n,S,G,X,x))) is Element of the carrier of (n,S,G,X,x)
x1 is Element of n
x1 is Element of the carrier of (n,S,G,X,x)
z is Element of the carrier of (n,S,G,X,x)
x1 + z is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . (x1,z) is Element of the carrier of (n,S,G,X,x)
z is V11() real ext-real set
y1 is Element of the carrier of (n,S,G,X,x)
z1 is Element of the carrier of (n,S,G,X,x)
y1 + z1 is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . (y1,z1) is Element of the carrier of (n,S,G,X,x)
z * (y1 + z1) is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) is non empty Relation-like [:REAL, the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[:REAL, the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the Mult of (n,S,G,X,x) . (z,(y1 + z1)) is set
z * y1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (z,y1) is set
z * z1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (z,z1) is set
(z * y1) + (z * z1) is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . ((z * y1),(z * z1)) is Element of the carrier of (n,S,G,X,x)
x1 is V11() real ext-real Element of REAL
x1 * y1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (x1,y1) is set
x1 * z1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (x1,z1) is set
(x1 * y1) + (x1 * z1) is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . ((x1 * y1),(x1 * z1)) is Element of the carrier of (n,S,G,X,x)
f is Element of n
f2 is Element of n
z is V11() real ext-real set
x1 is V11() real ext-real set
z * x1 is V11() real ext-real set
f is Element of the carrier of (n,S,G,X,x)
(z * x1) * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) is non empty Relation-like [:REAL, the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[:REAL, the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the Mult of (n,S,G,X,x) . ((z * x1),f) is set
x1 * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (x1,f) is set
z * (x1 * f) is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (z,(x1 * f)) is set
y1 is V11() real ext-real Element of REAL
z1 is V11() real ext-real Element of REAL
y1 * z1 is V11() real ext-real Element of REAL
(y1 * z1) * f is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . ((y1 * z1),f) is set
f3 is Element of n
x1 is Element of the carrier of (n,S,G,X,x)
1 * x1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) is non empty Relation-like [:REAL, the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[:REAL, the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the Mult of (n,S,G,X,x) . (1,x1) is set
z is V11() real ext-real Element of REAL
y1 is Element of n
z is Element of the carrier of (n,S,G,X,x)
dist (z,z) is V11() real ext-real Element of REAL
x1 is Element of the carrier of (n,S,G,X,x)
dist (z,x1) is V11() real ext-real Element of REAL
dist (x1,z) is V11() real ext-real Element of REAL
y1 is Element of the carrier of (n,S,G,X,x)
dist (z,y1) is V11() real ext-real Element of REAL
dist (x1,y1) is V11() real ext-real Element of REAL
(dist (z,x1)) + (dist (x1,y1)) is V11() real ext-real Element of REAL
S . (z,z) is set
z is V11() real ext-real Element of REAL
abs z is V11() real ext-real Element of REAL
x1 is Element of the carrier of (n,S,G,X,x)
z * x1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) is non empty Relation-like [:REAL, the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[:REAL, the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[:REAL, the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the Mult of (n,S,G,X,x) . (z,x1) is set
y1 is Element of the carrier of (n,S,G,X,x)
z * y1 is Element of the carrier of (n,S,G,X,x)
the Mult of (n,S,G,X,x) . (z,y1) is set
dist ((z * x1),(z * y1)) is V11() real ext-real Element of REAL
dist (x1,y1) is V11() real ext-real Element of REAL
(abs z) * (dist (x1,y1)) is V11() real ext-real Element of REAL
z1 is Element of n
f is Element of n
S . (z1,f) is V11() real ext-real Element of REAL
S . ((z * x1),(z * y1)) is set
(abs z) * 0 is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
K623((abs z)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K383() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total V53() V54() V55() V57() V59() Element of bool [:REAL,REAL:]
K151(K383(),(abs z),(id REAL)) is set
0 * K623((abs z)) is empty Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain set
(abs z) * H₁(z1,f) is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
(abs z) * (S . (z1,f)) is V11() real ext-real Element of REAL
y1 is Element of the carrier of (n,S,G,X,x)
x1 is Element of the carrier of (n,S,G,X,x)
dist (y1,x1) is V11() real ext-real Element of REAL
z is Element of the carrier of (n,S,G,X,x)
y1 + z is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) is non empty Relation-like [: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] -defined the carrier of (n,S,G,X,x) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):]
[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):] is non empty Relation-like set
[:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty Relation-like set
bool [:[: the carrier of (n,S,G,X,x), the carrier of (n,S,G,X,x):], the carrier of (n,S,G,X,x):] is non empty set
the addF of (n,S,G,X,x) . (y1,z) is Element of the carrier of (n,S,G,X,x)
x1 + z is Element of the carrier of (n,S,G,X,x)
the addF of (n,S,G,X,x) . (x1,z) is Element of the carrier of (n,S,G,X,x)
dist ((y1 + z),(x1 + z)) is V11() real ext-real Element of REAL
S . ((y1 + z),(x1 + z)) is set
S . (y1,x1) is set
n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () ()
the carrier of n is non empty set
G is V11() real ext-real Element of REAL
abs G is V11() real ext-real Element of REAL
S is Element of the carrier of n
G * S is Element of the carrier of n
the Mult of n is non empty Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]
[:REAL, the carrier of n:] is non empty Relation-like set
[:[:REAL, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty set
the Mult of n . (G,S) is set
(n,(G * S)) is V11() real ext-real Element of REAL
0. n is V108(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
dist ((0. n),(G * S)) is V11() real ext-real Element of REAL
(n,S) is V11() real ext-real Element of REAL
dist ((0. n),S) is V11() real ext-real Element of REAL
(abs G) * (n,S) is V11() real ext-real Element of REAL
G * (0. n) is Element of the carrier of n
the Mult of n . (G,(0. n)) is set
dist ((G * (0. n)),(G * S)) is V11() real ext-real Element of REAL
n is non empty right_complementable triangle Abelian add-associative right_zeroed () ()
the carrier of n is non empty set
G is Element of the carrier of n
S is Element of the carrier of n
G + S is Element of the carrier of n
the addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . (G,S) is Element of the carrier of n
(n,(G + S)) is V11() real ext-real Element of REAL
0. n is V108(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
dist ((0. n),(G + S)) is V11() real ext-real Element of REAL
(n,G) is V11() real ext-real Element of REAL
dist ((0. n),G) is V11() real ext-real Element of REAL
(n,S) is V11() real ext-real Element of REAL
dist ((0. n),S) is V11() real ext-real Element of REAL
(n,G) + (n,S) is V11() real ext-real Element of REAL
dist (G,(G + S)) is V11() real ext-real Element of REAL
(dist ((0. n),G)) + (dist (G,(G + S))) is V11() real ext-real Element of REAL
- G is Element of the carrier of n
G + (- G) is Element of the carrier of n
the addF of n . (G,(- G)) is Element of the carrier of n
(G + S) + (- G) is Element of the carrier of n
the addF of n . ((G + S),(- G)) is Element of the carrier of n
dist ((G + (- G)),((G + S) + (- G))) is V11() real ext-real Element of REAL
(n,G) + (dist ((G + (- G)),((G + S) + (- G)))) is V11() real ext-real Element of REAL
dist ((0. n),((G + S) + (- G))) is V11() real ext-real Element of REAL
(n,G) + (dist ((0. n),((G + S) + (- G)))) is V11() real ext-real Element of REAL
(- G) + G is Element of the carrier of n
the addF of n . ((- G),G) is Element of the carrier of n
S + ((- G) + G) is Element of the carrier of n
the addF of n . (S,((- G) + G)) is Element of the carrier of n
dist ((0. n),(S + ((- G) + G))) is V11() real ext-real Element of REAL
(n,G) + (dist ((0. n),(S + ((- G) + G)))) is V11() real ext-real Element of REAL
S + (0. n) is Element of the carrier of n
the addF of n . (S,(0. n)) is Element of the carrier of n
dist ((0. n),(S + (0. n))) is V11() real ext-real Element of REAL
(n,G) + (dist ((0. n),(S + (0. n)))) is V11() real ext-real Element of REAL
n is non empty right_complementable add-associative right_zeroed () ()
the carrier of n is non empty set
G is Element of the carrier of n
S is Element of the carrier of n
dist (G,S) is V11() real ext-real Element of REAL
S - G is Element of the carrier of n
- G is Element of the carrier of n
S + (- G) is Element of the carrier of n
the addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . (S,(- G)) is Element of the carrier of n
(n,(S - G)) is V11() real ext-real Element of REAL
0. n is V108(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
dist ((0. n),(S - G)) is V11() real ext-real Element of REAL
G + (- G) is Element of the carrier of n
the addF of n . (G,(- G)) is Element of the carrier of n
dist ((G + (- G)),(S + (- G))) is V11() real ext-real Element of REAL
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
[:(REAL n),(REAL n):] is non empty Relation-like set
Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:[:(REAL n),(REAL n):],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[:(REAL n),(REAL n):],REAL:] is non empty set
0* n is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
Seg n is V34() V41(n) V64() V65() V66() V67() V68() V69() Element of bool NAT
K153((Seg n),0) is Relation-like Seg n -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V34() FinSequence-like FinSubsequence-like V53() V54() V55() V56() Element of bool [:(Seg n),{0}:]
{0} is non empty functional V64() V65() V66() V67() V68() V69() set
[:(Seg n),{0}:] is Relation-like RAT -valued INT -valued V53() V54() V55() V56() set
bool [:(Seg n),{0}:] is non empty set
[:[:(REAL n),(REAL n):],(REAL n):] is non empty Relation-like set
bool [:[:(REAL n),(REAL n):],(REAL n):] is non empty set
G is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL n -valued Function-like total quasi_total Element of bool [:[:(REAL n),(REAL n):],(REAL n):]
[:REAL,(REAL n):] is non empty Relation-like set
[:[:REAL,(REAL n):],(REAL n):] is non empty Relation-like set
bool [:[:REAL,(REAL n):],(REAL n):] is non empty set
S is non empty Relation-like [:REAL,(REAL n):] -defined REAL n -valued Function-like total quasi_total Element of bool [:[:REAL,(REAL n):],(REAL n):]
((REAL n),(Pitag_dist n),(0* n),G,S) is non empty () ()
the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S) is non empty set
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x + y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) is non empty Relation-like [: the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S), the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] -defined the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S) -valued Function-like total quasi_total Element of bool [:[: the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S), the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):], the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):]
[: the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S), the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] is non empty Relation-like set
[:[: the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S), the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):], the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] is non empty Relation-like set
bool [:[: the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S), the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):], the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] is non empty set
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,y) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
(x + y) + z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x + y),z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 + y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K381() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K149(K381(),x1,y1) is set
G . ((x1 + y1),z) is set
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
(x1 + y1) + z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),(x1 + y1),z1) is set
y1 + z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),y1,z1) is set
x1 + (y1 + z1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),x1,(y1 + z1)) is set
G . (x,(y1 + z1)) is set
y + z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y,z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x + (y + z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,(y + z)) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x + y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,y) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z + x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),z,x1) is set
y + x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y,x) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
0. ((REAL n),(Pitag_dist n),(0* n),G,S) is V108(((REAL n),(Pitag_dist n),(0* n),G,S)) Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the ZeroF of ((REAL n),(Pitag_dist n),(0* n),G,S) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x + (0. ((REAL n),(Pitag_dist n),(0* n),G,S)) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,(0. ((REAL n),(Pitag_dist n),(0* n),G,S))) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
y + (n |-> 0) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K381(),y,(n |-> 0)) is set
y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
dist (y,z) is V11() real ext-real Element of REAL
(Pitag_dist n) . (y,z) is set
x1 - y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K382() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[:REAL,REAL:],REAL:]
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total V53() V54() V55() V57() V59() Element of bool [:REAL,REAL:]
K379() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K196(REAL,K381(),(id REAL),K379()) is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[:REAL,REAL:],REAL:]
K149(K382(),x1,y1) is set
K278(y1) is Relation-like Function-like V53() set
y1 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
- 1 is V11() real integer ext-real non positive set
(- 1) * y1 is Relation-like Function-like set
K623((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K383() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K151(K383(),(- 1),(id REAL)) is set
y1 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(x1,K278(y1)) is Relation-like Function-like set
|.(x1 - y1).| is V11() real ext-real non negative Element of REAL
x is V11() real ext-real Element of REAL
x * y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) is non empty Relation-like [:REAL, the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] -defined the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):], the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):]
[:REAL, the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] is non empty Relation-like set
[:[:REAL, the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):], the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] is non empty Relation-like set
bool [:[:REAL, the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):], the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S):] is non empty set
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,y) is set
x * x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(x) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),x,(id REAL)) is set
x1 * K623(x) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,z) is set
x * y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y1 * K623(x) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
dist ((x * y),(x * z)) is V11() real ext-real Element of REAL
(Pitag_dist n) . ((x * y),(x * z)) is set
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
x * z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
z1 * K623(x) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
x * f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
f * K623(x) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(x * z1) - (x * f) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K382(),(x * z1),(x * f)) is set
K278((x * f)) is Relation-like Function-like V53() set
(x * f) * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * (x * f) is Relation-like Function-like set
(x * f) * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249((x * z1),K278((x * f))) is Relation-like Function-like set
|.((x * z1) - (x * f)).| is V11() real ext-real non negative Element of REAL
- 1 is V11() real integer ext-real non positive Element of REAL
(- 1) * x is V11() real ext-real Element of REAL
((- 1) * x) * f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K623(((- 1) * x)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),((- 1) * x),(id REAL)) is set
f * K623(((- 1) * x)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(x * z1) + (((- 1) * x) * f) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K381(),(x * z1),(((- 1) * x) * f)) is set
|.((x * z1) + (((- 1) * x) * f)).| is V11() real ext-real non negative Element of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
f * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * f is Relation-like Function-like set
f * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x * (- f) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
(- f) * K623(x) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(x * z1) + (x * (- f)) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K381(),(x * z1),(x * (- f))) is set
|.((x * z1) + (x * (- f))).| is V11() real ext-real non negative Element of REAL
x * (x1 - y1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
(x1 - y1) * K623(x) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
|.(x * (x1 - y1)).| is V11() real ext-real non negative Element of REAL
abs x is V11() real ext-real Element of REAL
(abs x) * (dist (y,z)) is V11() real ext-real Element of REAL
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z + x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (z,x) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z1 + x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),z1,x1) is set
y + x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y,x) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y1 + x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),y1,x1) is set
dist (z,y) is V11() real ext-real Element of REAL
(Pitag_dist n) . (z,y) is set
z1 - y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),z1,y1) is set
K278(y1) is Relation-like Function-like V53() set
y1 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * y1 is Relation-like Function-like set
y1 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(z1,K278(y1)) is Relation-like Function-like set
|.(z1 - y1).| is V11() real ext-real non negative Element of REAL
f3 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
f3 + f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K381(),f3,f) is set
(f3 + f) - f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K382(),(f3 + f),f) is set
K278(f) is Relation-like Function-like V53() set
f * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * f is Relation-like Function-like set
f * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249((f3 + f),K278(f)) is Relation-like Function-like set
f2 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
((f3 + f) - f) - f2 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K382(),((f3 + f) - f),f2) is set
K278(f2) is Relation-like Function-like V53() set
f2 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * f2 is Relation-like Function-like set
f2 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(((f3 + f) - f),K278(f2)) is Relation-like Function-like set
|.(((f3 + f) - f) - f2).| is V11() real ext-real non negative Element of REAL
f + f2 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K381(),f,f2) is set
(f3 + f) - (f + f2) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K382(),(f3 + f),(f + f2)) is set
K278((f + f2)) is Relation-like Function-like V53() set
(f + f2) * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * (f + f2) is Relation-like Function-like set
(f + f2) * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249((f3 + f),K278((f + f2))) is Relation-like Function-like set
|.((f3 + f) - (f + f2)).| is V11() real ext-real non negative Element of REAL
(Pitag_dist n) . ((z1 + x1),(y1 + x1)) is V11() real ext-real Element of REAL
dist ((z + x),(y + x)) is V11() real ext-real Element of REAL
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
- y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
y * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * y is Relation-like Function-like set
y * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x + z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y - y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K382(),y,y) is set
K278(y) is Relation-like Function-like V53() set
K249(y,K278(y)) is Relation-like Function-like set
x is V11() real ext-real set
y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y + z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y,z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x1 is V11() real ext-real Element of REAL
x1 * (y + z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x1,(y + z)) is set
y1 + z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),y1,z1) is set
S . (x1,(y1 + z1)) is Relation-like NAT -defined Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of REAL n
f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
f2 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
f + f2 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K149(K381(),f,f2) is set
x1 * (f + f2) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K623(x1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),x1,(id REAL)) is set
(f + f2) * K623(x1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x1 * y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y1 * K623(x1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x1 * z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z1 * K623(x1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(x1 * y1) + (x1 * z1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),(x1 * y1),(x1 * z1)) is set
G . ((x1 * y1),(x1 * z1)) is Relation-like NAT -defined Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of REAL n
S . (x1,y) is set
G . ((S . (x1,y)),(x1 * z1)) is set
x1 * y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x1,y) is set
x1 * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x1,z) is set
(x1 * y) + (x1 * z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x1 * y),(x1 * z)) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x * (y + z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,(y + z)) is set
x * y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,y) is set
x * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,z) is set
(x * y) + (x * z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x * y),(x * z)) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x is V11() real ext-real set
y is V11() real ext-real set
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
x1 + y1 is V11() real ext-real Element of REAL
(x1 + y1) * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x1 + y1),z) is set
f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
(x1 + y1) * f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K623((x1 + y1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),(x1 + y1),(id REAL)) is set
f * K623((x1 + y1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x1 * z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(x1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),x1,(id REAL)) is set
z1 * K623(x1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
y1 * z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(y1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),y1,(id REAL)) is set
z1 * K623(y1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(x1 * z1) + (y1 * z1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),(x1 * z1),(y1 * z1)) is set
G . ((x1 * z1),(y1 * z1)) is Relation-like NAT -defined Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of REAL n
S . (x1,z) is set
G . ((S . (x1,z)),(y1 * z1)) is set
x1 * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x1,z) is set
y1 * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y1,z) is set
(x1 * z) + (y1 * z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x1 * z),(y1 * z)) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x + y is V11() real ext-real set
(x + y) * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x + y),z) is set
x * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,z) is set
y * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y,z) is set
(x * z) + (y * z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the addF of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x * z),(y * z)) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
x is V11() real ext-real set
y is V11() real ext-real set
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
x1 * y1 is V11() real ext-real Element of REAL
(x1 * y1) * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x1 * y1),z) is set
f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
(x1 * y1) * f is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K623((x1 * y1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),(x1 * y1),(id REAL)) is set
f * K623((x1 * y1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
y1 * z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(y1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),y1,(id REAL)) is set
z1 * K623(y1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x1 * (y1 * z1) is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(x1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),x1,(id REAL)) is set
(y1 * z1) * K623(x1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
S . (x1,(y1 * z1)) is Relation-like NAT -defined Function-like V34() V41(n) FinSequence-like FinSubsequence-like Element of REAL n
y1 * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y1,z) is set
x1 * (y1 * z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x1,(y1 * z)) is set
x * y is V11() real ext-real set
(x * y) * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . ((x * y),z) is set
y * z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (y,z) is set
x * (y * z) is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (x,(y * z)) is set
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
1 * x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
the Mult of ((REAL n),(Pitag_dist n),(0* n),G,S) . (1,x) is set
y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
1 * y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of n -tuples_on REAL
K623(1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),1,(id REAL)) is set
y * K623(1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
x is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
y is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
z is Element of the carrier of ((REAL n),(Pitag_dist n),(0* n),G,S)
dist (x,y) is V11() real ext-real Element of REAL
(Pitag_dist n) . (x,y) is set
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 - y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),x1,y1) is set
K278(y1) is Relation-like Function-like V53() set
y1 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * y1 is Relation-like Function-like set
y1 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(x1,K278(y1)) is Relation-like Function-like set
|.(x1 - y1).| is V11() real ext-real non negative Element of REAL
dist (x,z) is V11() real ext-real Element of REAL
(Pitag_dist n) . (x,z) is set
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 - z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),x1,z1) is set
K278(z1) is Relation-like Function-like V53() set
z1 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * z1 is Relation-like Function-like set
z1 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(x1,K278(z1)) is Relation-like Function-like set
|.(x1 - z1).| is V11() real ext-real non negative Element of REAL
x1 - x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),x1,x1) is set
K278(x1) is Relation-like Function-like V53() set
x1 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * x1 is Relation-like Function-like set
x1 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(x1,K278(x1)) is Relation-like Function-like set
|.(x1 - x1).| is empty V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V64() V65() V66() V67() V68() V69() V70() with_common_domain Element of REAL
(Pitag_dist n) . (x,x) is set
dist (x,x) is V11() real ext-real Element of REAL
(Pitag_dist n) . (x,y) is set
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 - y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),x1,y1) is set
K278(y1) is Relation-like Function-like V53() set
y1 * K379() is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
(- 1) * y1 is Relation-like Function-like set
y1 * K623((- 1)) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
K249(x1,K278(y1)) is Relation-like Function-like set
|.(x1 - y1).| is V11() real ext-real non negative Element of REAL
y1 - x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),y1,x1) is set
K249(y1,K278(x1)) is Relation-like Function-like set
|.(y1 - x1).| is V11() real ext-real non negative Element of REAL
(Pitag_dist n) . (y,x) is set
dist (y,x) is V11() real ext-real Element of REAL
dist (y,z) is V11() real ext-real Element of REAL
(Pitag_dist n) . (y,z) is set
y1 - z1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K382(),y1,z1) is set
K249(y1,K278(z1)) is Relation-like Function-like set
|.(y1 - z1).| is V11() real ext-real non negative Element of REAL
(dist (x,y)) + (dist (y,z)) is V11() real ext-real Element of REAL
x is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () ()
y is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of y is non empty set
[: the carrier of y, the carrier of y:] is non empty Relation-like set
the distance of y is non empty Relation-like [: the carrier of y, the carrier of y:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the carrier of y, the carrier of y:],REAL:]
[:[: the carrier of y, the carrier of y:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[: the carrier of y, the carrier of y:],REAL:] is non empty set
0. y is V108(y) Element of the carrier of y
the ZeroF of y is Element of the carrier of y
the addF of y is non empty Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like total quasi_total Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty Relation-like set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the Mult of y is non empty Relation-like [:REAL, the carrier of y:] -defined the carrier of y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of y:], the carrier of y:]
[:REAL, the carrier of y:] is non empty Relation-like set
[:[:REAL, the carrier of y:], the carrier of y:] is non empty Relation-like set
bool [:[:REAL, the carrier of y:], the carrier of y:] is non empty set
z is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
the addF of y . (z,x1) is set
z + x1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K149(K381(),z,x1) is set
z1 is V11() real ext-real Element of REAL
y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
the Mult of y . (z1,y1) is set
z1 * y1 is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(z1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K151(K383(),z1,(id REAL)) is set
y1 * K623(z1) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
G is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is non empty Relation-like set
the distance of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the carrier of G, the carrier of G:],REAL:]
[:[: the carrier of G, the carrier of G:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[: the carrier of G, the carrier of G:],REAL:] is non empty set
0. G is V108(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
the addF of G is non empty Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the Mult of G is non empty Relation-like [:REAL, the carrier of G:] -defined the carrier of G -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of G:], the carrier of G:]
[:REAL, the carrier of G:] is non empty Relation-like set
[:[:REAL, the carrier of G:], the carrier of G:] is non empty Relation-like set
bool [:[:REAL, the carrier of G:], the carrier of G:] is non empty set
S is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of S is non empty set
[: the carrier of S, the carrier of S:] is non empty Relation-like set
the distance of S is non empty Relation-like [: the carrier of S, the carrier of S:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:[: the carrier of S, the carrier of S:],REAL:]
[:[: the carrier of S, the carrier of S:],REAL:] is non empty Relation-like V53() V54() V55() set
bool [:[: the carrier of S, the carrier of S:],REAL:] is non empty set
0. S is V108(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
the addF of S is non empty Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like total quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty Relation-like set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the Mult of S is non empty Relation-like [:REAL, the carrier of S:] -defined the carrier of S -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of S:], the carrier of S:]
[:REAL, the carrier of S:] is non empty Relation-like set
[:[:REAL, the carrier of S:], the carrier of S:] is non empty Relation-like set
bool [:[:REAL, the carrier of S:], the carrier of S:] is non empty set
X is Element of the carrier of G
x is Element of the carrier of G
the addF of G . (X,x) is Element of the carrier of G
y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
z is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
y + z is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K381() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K149(K381(),y,z) is set
the addF of S . (X,x) is set
x is Element of the carrier of G
X is V11() real ext-real Element of REAL
the Mult of G . (X,x) is Element of the carrier of G
y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
X * y is Relation-like NAT -defined REAL -valued Function-like V34() V41(n) FinSequence-like FinSubsequence-like V53() V54() V55() Element of REAL n
K623(X) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K383() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V53() V54() V55() commutative associative Element of bool [:[:REAL,REAL:],REAL:]
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total V53() V54() V55() V57() V59() Element of bool [:REAL,REAL:]
K151(K383(),X,(id REAL)) is set
y * K623(X) is Relation-like NAT -defined REAL -valued Function-like V53() V54() V55() set
the Mult of S . (X,x) is set
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of (n) is non empty set
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V34() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
G is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
proj2 G is non empty set
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
((n)) is non empty functional Element of bool (Funcs ( the carrier of (n), the carrier of (n)))
the carrier of (n) is non empty set
Funcs ( the carrier of (n), the carrier of (n)) is non empty functional FUNCTION_DOMAIN of the carrier of (n), the carrier of (n)
bool (Funcs ( the carrier of (n), the carrier of (n))) is non empty set
G is Relation-like Function-like Element of ((n))
S is Relation-like Function-like Element of ((n))
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
x is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
X * x is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
y is Relation-like Function-like Element of ((n))
x * X is Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one set
[:((n)),((n)):] is non empty Relation-like set
[:[:((n)),((n)):],((n)):] is non empty Relation-like set
bool [:[:((n)),((n)):],((n)):] is non empty set
G is non empty Relation-like [:((n)),((n)):] -defined ((n)) -valued Function-like total quasi_total Element of bool [:[:((n)),((n)):],((n)):]
multMagma(# ((n)),G #) is strict multMagma
S is strict multMagma
the carrier of S is set
the multF of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is Relation-like set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
X is Relation-like Function-like set
x is Relation-like Function-like set
the multF of S . (X,x) is set
x * X is Relation-like Function-like set
G . (X,x) is set
y is Relation-like Function-like set
z is Relation-like Function-like set
z * y is Relation-like Function-like set
X is Relation-like Function-like set
x is Relation-like Function-like set
the multF of S . (X,x) is set
x * X is Relation-like Function-like set
S is strict multMagma
the carrier of S is set
the multF of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is Relation-like set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
X is strict multMagma
the carrier of X is set
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
the multF of S . (x,y) is Element of the carrier of S
x1 is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
z is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
z * x1 is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
the multF of X . (x,y) is set
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is strict multMagma
the carrier of (n) is set
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
((n)) is non empty functional Element of bool (Funcs ( the carrier of (n), the carrier of (n)))
the carrier of (n) is non empty set
Funcs ( the carrier of (n), the carrier of (n)) is non empty functional FUNCTION_DOMAIN of the carrier of (n), the carrier of (n)
bool (Funcs ( the carrier of (n), the carrier of (n))) is non empty set
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty strict multMagma
the carrier of (n) is non empty set
G is Element of the carrier of (n)
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
((n)) is non empty functional Element of bool (Funcs ( the carrier of (n), the carrier of (n)))
the carrier of (n) is non empty set
Funcs ( the carrier of (n), the carrier of (n)) is non empty functional FUNCTION_DOMAIN of the carrier of (n), the carrier of (n)
bool (Funcs ( the carrier of (n), the carrier of (n))) is non empty set
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
S is Element of the carrier of (n)
y is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
x is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
x * y is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
X is Element of the carrier of (n)
z is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
y * z is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
G * S is Element of the carrier of (n)
the multF of (n) is non empty Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty Relation-like set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty set
the multF of (n) . (G,S) is Element of the carrier of (n)
(G * S) * X is Element of the carrier of (n)
the multF of (n) . ((G * S),X) is Element of the carrier of (n)
the multF of (n) . ((x * y),X) is set
(x * y) * z is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
x * (y * z) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
the multF of (n) . (G,(y * z)) is set
S * X is Element of the carrier of (n)
the multF of (n) . (S,X) is Element of the carrier of (n)
G * (S * X) is Element of the carrier of (n)
the multF of (n) . (G,(S * X)) is Element of the carrier of (n)
id (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
id the carrier of (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
G is Element of the carrier of (n)
S is Element of the carrier of (n)
S * G is Element of the carrier of (n)
the multF of (n) . (S,G) is Element of the carrier of (n)
G * S is Element of the carrier of (n)
the multF of (n) . (G,S) is Element of the carrier of (n)
X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
X * (id the carrier of (n)) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
(id the carrier of (n)) * X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
proj2 X is non empty set
[#] (n) is non empty non proper Element of bool the carrier of (n)
bool the carrier of (n) is non empty set
X " is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total quasi_total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
x is Element of the carrier of (n)
S * x is Element of the carrier of (n)
the multF of (n) . (S,x) is Element of the carrier of (n)
x * S is Element of the carrier of (n)
the multF of (n) . (x,S) is Element of the carrier of (n)
X * (X ") is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
(X ") * X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total total quasi_total quasi_total onto onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
dom X is non empty Element of bool the carrier of (n)
id (dom X) is non empty Relation-like dom X -defined dom X -valued Function-like one-to-one total quasi_total Element of bool [:(dom X),(dom X):]
[:(dom X),(dom X):] is non empty Relation-like set
bool [:(dom X),(dom X):] is non empty set
G is Element of the carrier of (n)
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty strict Group-like associative multMagma
1_ (n) is Element of the carrier of (n)
the carrier of (n) is non empty set
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
id (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
the carrier of (n) is non empty set
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
id the carrier of (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
((n)) is non empty functional Element of bool (Funcs ( the carrier of (n), the carrier of (n)))
Funcs ( the carrier of (n), the carrier of (n)) is non empty functional FUNCTION_DOMAIN of the carrier of (n), the carrier of (n)
bool (Funcs ( the carrier of (n), the carrier of (n))) is non empty set
S is Element of the carrier of (n)
G is Element of the carrier of (n)
S * G is Element of the carrier of (n)
the multF of (n) is non empty Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty Relation-like set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty set
the multF of (n) . (S,G) is Element of the carrier of (n)
X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
X * (id the carrier of (n)) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
G * S is Element of the carrier of (n)
the multF of (n) . (G,S) is Element of the carrier of (n)
(id the carrier of (n)) * X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty strict Group-like associative multMagma
the carrier of (n) is non empty set
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of (n) is non empty set
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
G is Element of the carrier of (n)
G " is Element of the carrier of (n)
S is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
S " is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
((n)) is non empty functional Element of bool (Funcs ( the carrier of (n), the carrier of (n)))
Funcs ( the carrier of (n), the carrier of (n)) is non empty functional FUNCTION_DOMAIN of the carrier of (n), the carrier of (n)
bool (Funcs ( the carrier of (n), the carrier of (n))) is non empty set
X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
proj2 X is non empty set
[#] (n) is non empty non proper Element of bool the carrier of (n)
bool the carrier of (n) is non empty set
x is Element of the carrier of (n)
x * G is Element of the carrier of (n)
the multF of (n) is non empty Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty Relation-like set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty set
the multF of (n) . (x,G) is Element of the carrier of (n)
(S ") * X is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
dom X is non empty Element of bool the carrier of (n)
id (dom X) is non empty Relation-like dom X -defined dom X -valued Function-like one-to-one total quasi_total Element of bool [:(dom X),(dom X):]
[:(dom X),(dom X):] is non empty Relation-like set
bool [:(dom X),(dom X):] is non empty set
id (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
id the carrier of (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
1_ (n) is Element of the carrier of (n)
G * x is Element of the carrier of (n)
the multF of (n) . (G,x) is Element of the carrier of (n)
X * (S ") is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty strict Group-like associative multMagma
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of (n) is non empty set
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
G is non empty Group-like associative Subgroup of (n)
the carrier of G is non empty set
S is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]
X is Element of the carrier of (n)
x is Element of the carrier of (n)
[X,x] is V26() Element of [: the carrier of (n), the carrier of (n):]
{X,x} is non empty set
{X} is non empty set
{{X,x},{X}} is non empty set
y is Relation-like Function-like set
y . X is set
S is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]
X is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]
x is set
y is set
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
z is Element of the carrier of (n)
x1 is Element of the carrier of (n)
y1 is Relation-like Function-like set
y1 . z is set
z is Element of the carrier of (n)
x1 is Element of the carrier of (n)
y1 is Relation-like Function-like set
y1 . z is set
n is ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT
(n) is non empty strict Group-like associative multMagma
(n) is non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () () () ()
the carrier of (n) is non empty set
G is non empty Group-like associative Subgroup of (n)
(n,G) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
bool [: the carrier of (n), the carrier of (n):] is non empty set
x is set
1_ (n) is Element of the carrier of (n)
the carrier of (n) is non empty set
id (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
id the carrier of (n) is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (n), the carrier of (n):]
the carrier of G is non empty set
y is Element of the carrier of (n)
(id (n)) . y is Element of the carrier of (n)
[x,x] is V26() set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
field (n,G) is set
dom (n,G) is Element of bool the carrier of (n)
bool the carrier of (n) is non empty set
x is set
y is set
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
z is Element of the carrier of (n)
x1 is Element of the carrier of (n)
y1 is Relation-like Function-like set
y1 . z is set
z1 is Element of the carrier of G
((n)) is non empty functional Element of bool (Funcs ( the carrier of (n), the carrier of (n)))
Funcs ( the carrier of (n), the carrier of (n)) is non empty functional FUNCTION_DOMAIN of the carrier of (n), the carrier of (n)
bool (Funcs ( the carrier of (n), the carrier of (n))) is non empty set
f2 is non empty Relation-like the carrier of (n) -defined the carrier of (n) -valued Function-like one-to-one total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
dom f2 is non empty Element of bool the carrier of (n)
y1 " is Relation-like Function-like set
(y1 ") . x1 is set
z1 " is Element of the carrier of G
f is Element of the carrier of (n)
f " is Element of the carrier of (n)
f2 " is non empty Relation-like the carrier of (n) -defined the carrier of (n) -defined the carrier of (n) -valued the carrier of (n) -valued Function-like one-to-one total quasi_total quasi_total onto bijective ((n)) Element of bool [: the carrier of (n), the carrier of (n):]
[y,x] is V26() set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
x is set
y is set
z is set
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,z] is V26() set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
x1 is Element of the carrier of (n)
y1 is Element of the carrier of (n)
f is Relation-like Function-like set
f . x1 is set
f2 is Element of the carrier of G
z1 is Element of the carrier of (n)
g is Relation-like Function-like set
g . y1 is set
g2 is Element of the carrier of G
g3 is Element of the carrier of (n)
f3 is Element of the carrier of (n)
g3 * f3 is Element of the carrier of (n)
the multF of (n) is non empty Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like total quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is non empty Relation-like set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty Relation-like set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty set
the multF of (n) . (g3,f3) is Element of the carrier of (n)
f * g is Relation-like Function-like set
proj1 f is set
(f * g) . x1 is set
[x,z] is V26() set
{x,z} is non empty set
{{x,z},{x}} is non empty set