:: SPRECT_5 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty Element of K27(REAL)

K27(REAL) is set

NAT is V6() V7() V8() non empty set

K27(NAT) is set

K27(NAT) is set

1 is V6() V7() V8() V12() non empty ext-real positive V39() V43() Element of NAT

K28(1,1) is set

K27(K28(1,1)) is set

K28(K28(1,1),1) is set

K27(K28(K28(1,1),1)) is set

K28(K28(1,1),REAL) is set

K27(K28(K28(1,1),REAL)) is set

K28(REAL,REAL) is set

K28(K28(REAL,REAL),REAL) is set

K27(K28(K28(REAL,REAL),REAL)) is set

2 is V6() V7() V8() V12() non empty ext-real positive V39() V43() Element of NAT

K28(2,2) is set

K28(K28(2,2),REAL) is set

K27(K28(K28(2,2),REAL)) is set

COMPLEX is set

RAT is set

INT is set

K27(K28(REAL,REAL)) is set

TOP-REAL 2 is V47() V52() V161() L15()

the U1 of (TOP-REAL 2) is non empty V19() set

K27( the U1 of (TOP-REAL 2)) is set

K28( the U1 of (TOP-REAL 2),REAL) is set

K27(K28( the U1 of (TOP-REAL 2),REAL)) is set

{} is V6() V7() V8() V10() V11() V12() Function-like functional empty ext-real V39() V43() set

Seg 1 is Element of K27(NAT)

4 is V6() V7() V8() V12() non empty ext-real positive V39() V43() Element of NAT

0 is V6() V7() V8() V10() V11() V12() Function-like functional empty ext-real V39() V43() Element of NAT

len {} is V29() set

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 is Element of z

p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g | (p3 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng (g | (p3 .. g)) is set

p2 .. (g | (p3 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len (g | (p3 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng g is set

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g :- p2 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

p3 is Element of z

p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 .. (g :- p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(p3 .. g) - (p2 .. g) is ext-real V39() V43() set

((p3 .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set

g | (p2 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

g /^ (p2 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

(g | (p2 .. g)) ^ (g /^ (p2 .. g)) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

len g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len (g | (p2 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (g | (p2 .. g)) is set

rng (g /^ (p2 .. g)) is set

(rng (g | (p2 .. g))) \/ (rng (g /^ (p2 .. g))) is set

(rng (g /^ (p2 .. g))) \ (rng (g | (p2 .. g))) is Element of K27((rng (g /^ (p2 .. g))))

K27((rng (g /^ (p2 .. g)))) is set

p3 .. (g /^ (p2 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(p2 .. g) + (p3 .. (g /^ (p2 .. g))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

{p2} is non empty set

<*p2*> is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng <*p2*> is set

(rng (g /^ (p2 .. g))) \ (rng <*p2*>) is Element of K27((rng (g /^ (p2 .. g))))

<*p2*> ^ (g /^ (p2 .. g)) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

len <*p2*> is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len <*p2*>) + (p3 .. (g /^ (p2 .. g))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng g is set

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 is Element of z

p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g -: p3 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

p2 .. (g -: p3) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g | (p3 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng (g | (p3 .. g)) is set

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng g is set

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (g,p2) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

p3 is Element of z

p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(p3 .. g) - (p2 .. g) is ext-real V39() V43() set

((p3 .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set

g :- p2 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

g -: p2 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

(g -: p2) /^ 1 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

(g :- p2) ^ ((g -: p2) /^ 1) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng (g :- p2) is set

p3 .. (g :- p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng g is set

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (g,p2) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

p3 is Element of z

p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

j is Element of z

j .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

j .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(j .. g) - (p2 .. g) is ext-real V39() V43() set

(p3 .. g) - (p2 .. g) is ext-real V39() V43() set

((p3 .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set

((j .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

rng g is set

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (g,p2) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z

p3 is Element of z

p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

j is Element of z

j .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

j .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is non empty set

g is V1() V4( NAT ) V5(z) Function-like FinSequence-like circular FinSequence of z

rng g is set

len g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is Element of z

p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g /. (len g) is Element of z

g /. 1 is Element of z

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

z /^ 1 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

g is set

K49((z /^ 1)) is set

p2 is set

(z /^ 1) . g is set

(z /^ 1) . p2 is set

dom (z /^ 1) is Element of K27(NAT)

p3 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

dom z is V19() Element of K27(NAT)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

j + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. (p3 + 1) is Element of the U1 of (TOP-REAL 2)

(z /^ 1) /. p3 is Element of the U1 of (TOP-REAL 2)

(z /^ 1) . j is set

(z /^ 1) /. j is Element of the U1 of (TOP-REAL 2)

z /. (j + 1) is Element of the U1 of (TOP-REAL 2)

z /. (j + 1) is Element of the U1 of (TOP-REAL 2)

(z /^ 1) /. j is Element of the U1 of (TOP-REAL 2)

(z /^ 1) . p3 is set

(z /^ 1) /. p3 is Element of the U1 of (TOP-REAL 2)

z /. (p3 + 1) is Element of the U1 of (TOP-REAL 2)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

rng z is V19() set

z /. 1 is Element of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len z) + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g is Element of the U1 of (TOP-REAL 2)

g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

(z /. 1) .. (Rotate (z,g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

((len z) + 1) - (g .. z) is ext-real V39() V43() set

1 + (len z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(1 + (len z)) -' (g .. z) is V6() V7() V8() V12() ext-real non negative V39() V43() Element of NAT

(g .. z) - 1 is ext-real V39() V43() set

(1 + (len z)) - (g .. z) is ext-real V39() V43() set

((1 + (len z)) -' (g .. z)) + ((g .. z) - 1) is ext-real V39() V43() set

len (Rotate (z,g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(g .. z) + 0 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. (g .. z) is Element of the U1 of (TOP-REAL 2)

(len z) - (g .. z) is ext-real V39() V43() set

1 + ((len z) - (g .. z)) is ext-real V39() V43() set

1 + 0 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

dom (Rotate (z,g)) is V19() Element of K27(NAT)

(Rotate (z,g)) /. ((1 + (len z)) -' (g .. z)) is Element of the U1 of (TOP-REAL 2)

(Rotate (z,g)) . ((1 + (len z)) -' (g .. z)) is set

p3 is set

(Rotate (z,g)) . p3 is set

j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(Rotate (z,g)) /. j is Element of the U1 of (TOP-REAL 2)

j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(Rotate (z,g)) /. j is Element of the U1 of (TOP-REAL 2)

j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(Rotate (z,g)) <- (z /. 1) is set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

rng z is V19() set

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g is Element of the U1 of (TOP-REAL 2)

g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len z) + (g .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is Element of the U1 of (TOP-REAL 2)

p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,p2) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

g .. (Rotate (z,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

((len z) + (g .. z)) - (p2 .. z) is ext-real V39() V43() set

z -: p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

g .. (z -: p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (z -: p2) is set

z :- p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

(z -: p2) /^ 1 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

(z :- p2) ^ ((z -: p2) /^ 1) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

g .. ((z -: p2) /^ 1) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

1 + (g .. ((z -: p2) /^ 1)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

{p2} is non empty set

<*p2*> is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

rng <*p2*> is set

z /^ 1 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like one-to-one FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

rng (z /^ 1) is set

(z /^ 1) -| p2 is V1() Function-like FinSequence-like set

((z /^ 1) -| p2) ^ <*p2*> is V1() Function-like FinSequence-like set

p2 .. (z /^ 1) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(z /^ 1) | (p2 .. (z /^ 1)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

(z /^ 1) -: p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

rng ((z /^ 1) -: p2) is set

rng ((z /^ 1) -| p2) is set

(rng ((z /^ 1) -| p2)) \/ (rng <*p2*>) is set

(z /^ 1) |-- p2 is V1() Function-like FinSequence-like set

rng ((z /^ 1) |-- p2) is set

(z /^ 1) :- p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

<*p2*> ^ ((z /^ 1) |-- p2) is V1() Function-like FinSequence-like set

rng ((z /^ 1) :- p2) is set

(rng <*p2*>) \/ (rng ((z /^ 1) |-- p2)) is set

rng ((z -: p2) /^ 1) is set

rng (z :- p2) is set

(rng ((z -: p2) /^ 1)) \ (rng (z :- p2)) is Element of K27((rng ((z -: p2) /^ 1)))

K27((rng ((z -: p2) /^ 1))) is set

len (z :- p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len (z :- p2)) + (g .. ((z -: p2) /^ 1)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len z) - (p2 .. z) is ext-real V39() V43() set

((len z) - (p2 .. z)) + 1 is ext-real V39() V43() set

(g .. z) - 1 is ext-real V39() V43() set

(((len z) - (p2 .. z)) + 1) + ((g .. z) - 1) is ext-real V39() V43() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

rng z is V19() set

g is Element of the U1 of (TOP-REAL 2)

g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is Element of the U1 of (TOP-REAL 2)

p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,p2) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

g .. (Rotate (z,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 is Element of the U1 of (TOP-REAL 2)

p3 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 .. (Rotate (z,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (Rotate (z,p2)) is V19() set

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(p3 .. z) + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len z) + (g .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(p3 .. z) - (p2 .. z) is ext-real V39() V43() set

((p3 .. z) - (p2 .. z)) + 1 is ext-real V39() V43() set

((p3 .. z) + 1) - (p2 .. z) is ext-real V39() V43() set

((len z) + (g .. z)) - (p2 .. z) is ext-real V39() V43() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

rng z is V19() set

g is Element of the U1 of (TOP-REAL 2)

g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is Element of the U1 of (TOP-REAL 2)

p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 is Element of the U1 of (TOP-REAL 2)

p3 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,p3) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

p2 .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

g .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(len z) + (g .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

((len z) + (g .. z)) - (p3 .. z) is ext-real V39() V43() set

(len z) + (p2 .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

((len z) + (p2 .. z)) - (p3 .. z) is ext-real V39() V43() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

rng z is V19() set

g is Element of the U1 of (TOP-REAL 2)

g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is Element of the U1 of (TOP-REAL 2)

p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p3 is Element of the U1 of (TOP-REAL 2)

p3 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,p3) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

g .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

dom z is V19() Element of K27(NAT)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

rng (Rotate (z,(N-min (L~ z)))) is V19() set

W-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

N-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (Rotate (z,(N-min (L~ z)))) is V19() set

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

N-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

rng (Rotate (z,(N-min (L~ z)))) is V19() set

(N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (Rotate (z,(N-min (L~ z)))) is V19() set

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

rng (Rotate (z,(N-min (L~ z)))) is V19() set

(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

rng (Rotate (z,(N-min (L~ z)))) is V19() set

S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng z is V19() set

dom z is V19() Element of K27(NAT)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

E-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

S-min (L~ z) is Element of the U1 of (TOP-REAL 2)

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

rng (Rotate (z,(N-min (L~ z)))) is V19() set

(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(N-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(W-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (Rotate (z,(W-min (L~ z)))) is V19() set

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

W-max (L~ z) is Element of the U1 of (TOP-REAL 2)

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

W-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

rng (Rotate (z,(W-min (L~ z)))) is V19() set

(W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ z) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

W-min (L~ z) is Element of the U1 of (TOP-REAL 2)

Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))

rng z is V19() set

(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)

W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

N-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)

(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

rng (Rotate (z,(W-min (L~ z)))) is V19() set

len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

z /. p2 is Element of the U1 of (TOP-REAL 2)

Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

z /. 1 is Element of the U1 of (TOP-REAL 2)

L~ z is Element of K27( the U1 of (TOP-REAL 2))

S-max (L~ z) is Element of the U1 of (TOP-REAL 2)

N-max (L~ z) is Element of the U1 of (TOP-REAL 2)

E-max (L~ z) is Element of the U1 of (TOP-REAL 2)

(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT

(N-max (L~ z)) .. z is