:: GOBRD11 semantic presentation

REAL is V110() V111() V112() V116() set
NAT is V110() V111() V112() V113() V114() V115() V116() Element of bool REAL
bool REAL is non empty set
COMPLEX is V110() V116() set
omega is V110() V111() V112() V113() V114() V115() V116() set
bool omega is non empty set
1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set

bool is non empty set
2 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
RAT is V110() V111() V112() V113() V116() set
INT is V110() V111() V112() V113() V114() V116() set
bool NAT is non empty set
bool is non empty set
TOP-REAL 2 is non empty TopSpace-like V136() V161() V162() V163() V164() V165() V166() V167() strict RLTopStruct
the carrier of () is non empty set
K295( the carrier of ()) is M12( the carrier of ())
bool the carrier of () is non empty set
{} is empty V110() V111() V112() V113() V114() V115() V116() set
the empty V110() V111() V112() V113() V114() V115() V116() set is empty V110() V111() V112() V113() V114() V115() V116() set
0 is empty natural V14() real ext-real non positive non negative V108() V109() V110() V111() V112() V113() V114() V115() V116() Element of NAT
K396(1,2) is V14() real ext-real non negative Element of COMPLEX
|[1,0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
K47(1) is V14() real ext-real non positive set
|[K47(1),1]| is V43(2) V100() FinSequence-like Element of the carrier of ()
sqrt 2 is V14() real ext-real Element of REAL

REAL 2 is non empty FinSequence-membered M12( REAL )
K296(2,REAL) is FinSequence-membered M12( REAL )
Pitag_dist 2 is V19() V22([:(REAL 2),(REAL 2):]) V23( REAL ) V24() V33([:(REAL 2),(REAL 2):], REAL ) Element of bool [:[:(REAL 2),(REAL 2):],REAL:]
[:(REAL 2),(REAL 2):] is non empty set
[:[:(REAL 2),(REAL 2):],REAL:] is set
bool [:[:(REAL 2),(REAL 2):],REAL:] is non empty set
MetrStruct(# (REAL 2),() #) is strict MetrStruct
the carrier of () is non empty set
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of the carrier of i
Component_of G is Element of bool the carrier of i
bool (bool the carrier of i) is non empty set
Y is Element of bool (bool the carrier of i)
union Y is set
x is set
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
Y is Element of bool the carrier of i
j is Element of bool the carrier of i
G is Element of bool the carrier of i
Cl j is Element of bool the carrier of i
Cl G is Element of bool the carrier of i
(Cl j) /\ (Cl G) is Element of bool the carrier of i
x is Element of the carrier of i
p is Element of bool the carrier of i
Cl Y is Element of bool the carrier of i
Component_of x is Element of bool the carrier of i
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of bool the carrier of i
j \/ G is Element of bool the carrier of i
{j,G} is non empty set
Y is set
bool (bool the carrier of i) is non empty set
Y is Element of bool (bool the carrier of i)
x is Element of bool (bool the carrier of i)
p is Element of bool the carrier of i
union x is set
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of bool the carrier of i
j \/ G is Element of bool the carrier of i
Y is Element of bool the carrier of i
Down ((j \/ G),Y) is Element of bool the carrier of (i | Y)
i | Y is strict TopSpace-like SubSpace of i
the carrier of (i | Y) is set
bool the carrier of (i | Y) is non empty set
Down (j,Y) is Element of bool the carrier of (i | Y)
Down (G,Y) is Element of bool the carrier of (i | Y)
(Down (j,Y)) \/ (Down (G,Y)) is Element of bool the carrier of (i | Y)
G /\ Y is Element of bool the carrier of i
(j \/ G) /\ Y is Element of bool the carrier of i
j /\ Y is Element of bool the carrier of i
i is non empty TopSpace-like TopStruct
the carrier of i is non empty set
bool the carrier of i is non empty set
j is Element of bool the carrier of i
G is Element of bool the carrier of i
j /\ G is Element of bool the carrier of i
Y is Element of bool the carrier of i
Down ((j /\ G),Y) is Element of bool the carrier of (i | Y)
i | Y is strict TopSpace-like SubSpace of i
the carrier of (i | Y) is set
bool the carrier of (i | Y) is non empty set
Down (j,Y) is Element of bool the carrier of (i | Y)
Down (G,Y) is Element of bool the carrier of (i | Y)
(Down (j,Y)) /\ (Down (G,Y)) is Element of bool the carrier of (i | Y)
(j /\ G) /\ Y is Element of bool the carrier of i
Y /\ Y is Element of bool the carrier of i
G /\ (Y /\ Y) is Element of bool the carrier of i
j /\ (G /\ (Y /\ Y)) is Element of bool the carrier of i
G /\ Y is Element of bool the carrier of i
(G /\ Y) /\ Y is Element of bool the carrier of i
j /\ ((G /\ Y) /\ Y) is Element of bool the carrier of i
j /\ Y is Element of bool the carrier of i
(j /\ Y) /\ (G /\ Y) is Element of bool the carrier of i
i is non empty V19() V22( NAT ) V23( the carrier of ()) V24() non constant FinSequence-like V180( the carrier of ()) special unfolded s.c.c. standard FinSequence of the carrier of ()
L~ i is Element of bool the carrier of ()
(L~ i) ` is Element of bool the carrier of ()

width (GoB i) is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(width (GoB i)) -' 1 is natural V14() real ext-real non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,((width (GoB i)) -' 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(GoB i) * (1,(width (GoB i))) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i)))) is V43(2) V100() FinSequence-like Element of the carrier of ()
1 / 2 is V14() real ext-real non negative Element of REAL
(1 / 2) * (((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i))))) is V43(2) V100() FinSequence-like Element of the carrier of ()
((1 / 2) * (((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i)))))) - |[1,0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
- 1 is V14() real ext-real non positive Element of REAL
|[(- 1),1]| is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(width (GoB i)))) + |[(- 1),1]| is V43(2) V100() FinSequence-like Element of the carrier of ()
LSeg ((((1 / 2) * (((GoB i) * (1,((width (GoB i)) -' 1))) + ((GoB i) * (1,(width (GoB i)))))) - |[1,0]|),(((GoB i) * (1,(width (GoB i)))) + |[(- 1),1]|)) is non empty V220( TOP-REAL 2) Element of bool the carrier of ()
i is non empty V19() V22( NAT ) V23( the carrier of ()) V24() non constant FinSequence-like V180( the carrier of ()) special unfolded s.c.c. standard FinSequence of the carrier of ()
L~ i is Element of bool the carrier of ()
(L~ i) ` is Element of bool the carrier of ()
i is non empty V19() V22( NAT ) V23( the carrier of ()) V24() non constant FinSequence-like V180( the carrier of ()) special unfolded s.c.c. standard FinSequence of the carrier of ()

len (GoB i) is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width (GoB i) is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (cell ((GoB i),b1,b2)) where b1, b2 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( b1 <= len (GoB i) & b2 <= width (GoB i) ) } is set
union { (cell ((GoB i),b1,b2)) where b1, b2 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( b1 <= len (GoB i) & b2 <= width (GoB i) ) } is set
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of ()
x `1 is V14() real ext-real Element of REAL
(GoB i) * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,1)) `1 is V14() real ext-real Element of REAL
(GoB i) * ((len (GoB i)),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((len (GoB i)),1)) `1 is V14() real ext-real Element of REAL
1 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(1 + 1) - 1 is V14() real ext-real Element of REAL
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G0 - 1 is V14() real ext-real Element of REAL
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
u + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
(u + 1) + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (((u + 1) + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (((u + 1) + 1),1)) `1 is V14() real ext-real Element of REAL
0 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
0 + 1 is non empty natural V14() real ext-real positive non negative V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((0 + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((0 + 1),1)) `1 is V14() real ext-real Element of REAL
(G0 - 1) + 1 is V14() real ext-real Element of REAL
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (G0,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (G0,1)) `1 is V14() real ext-real Element of REAL
G0 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((G0 + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((G0 + 1),1)) `1 is V14() real ext-real Element of REAL

width G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (G0,0) is Element of bool the carrier of ()
G0 * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(G0 * (1,1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (G0 * (1,1)) `1 } is set
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= ((GoB i) * (1,1)) `1 } is set
v_strip ((GoB i),0) is Element of bool the carrier of ()

width G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
len G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (G0,(len G0)) is Element of bool the carrier of ()
G0 * ((len G0),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(G0 * ((len G0),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (G0 * ((len G0),1)) `1 <= b1 } is set
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
(GoB i) * ((len G0),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((len G0),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ((GoB i) * ((len G0),1)) `1 <= b1 } is set
v_strip ((GoB i),(len (GoB i))) is Element of bool the carrier of ()
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (u,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (u,1)) `1 is V14() real ext-real Element of REAL
u + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (u,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (u,1)) `1 is V14() real ext-real Element of REAL
u + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()

G0 * (u,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(G0 * (u,1)) `1 is V14() real ext-real Element of REAL
G0 * ((u + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(G0 * ((u + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (G0 * (u,1)) `1 <= b1 & b1 <= (G0 * ((u + 1),1)) `1 ) } is set
width G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (G0,u) is Element of bool the carrier of ()
v_strip ((GoB i),u) is Element of bool the carrier of ()
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (G0,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (G0,1)) `1 is V14() real ext-real Element of REAL
G0 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((G0 + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((G0 + 1),1)) `1 is V14() real ext-real Element of REAL
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),G0) is Element of bool the carrier of ()
u is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),u) is Element of bool the carrier of ()
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (v,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (v,1)) `1 is V14() real ext-real Element of REAL
v + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * ((v + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * ((v + 1),1)) `1 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),G00) is Element of bool the carrier of ()
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip ((GoB i),G0) is Element of bool the carrier of ()
x `2 is V14() real ext-real Element of REAL
((GoB i) * (1,1)) `2 is V14() real ext-real Element of REAL
(GoB i) * (1,(width (GoB i))) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(width (GoB i)))) `2 is V14() real ext-real Element of REAL
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v - 1 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G00 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
(G00 + 1) + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,((G00 + 1) + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,((G00 + 1) + 1))) `2 is V14() real ext-real Element of REAL
(GoB i) * (1,(0 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(0 + 1))) `2 is V14() real ext-real Element of REAL
(v - 1) + 1 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,v) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,v)) `2 is V14() real ext-real Element of REAL
v + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(v + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(v + 1))) `2 is V14() real ext-real Element of REAL

len v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (v,0) is Element of bool the carrier of ()
v * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(v * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (v * (1,1)) `2 } is set
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= ((GoB i) * (1,1)) `2 } is set
h_strip ((GoB i),0) is Element of bool the carrier of ()

len v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (v,()) is Element of bool the carrier of ()
v * (1,()) is V43(2) V100() FinSequence-like Element of the carrier of ()
(v * (1,())) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (v * (1,())) `2 <= b2 } is set
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
(GoB i) * (1,()) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,())) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ((GoB i) * (1,())) `2 <= b2 } is set
h_strip ((GoB i),(width (GoB i))) is Element of bool the carrier of ()
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,G00) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,G00)) `2 is V14() real ext-real Element of REAL
G00 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,G00) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,G00)) `2 is V14() real ext-real Element of REAL
G00 + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()

v * (1,G00) is V43(2) V100() FinSequence-like Element of the carrier of ()
(v * (1,G00)) `2 is V14() real ext-real Element of REAL
v * (1,(G00 + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(v * (1,(G00 + 1))) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (v * (1,G00)) `2 <= b2 & b2 <= (v * (1,(G00 + 1))) `2 ) } is set
len v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (v,G00) is Element of bool the carrier of ()
h_strip ((GoB i),G00) is Element of bool the carrier of ()
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,v) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,v)) `2 is V14() real ext-real Element of REAL
v + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(v + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(v + 1))) `2 is V14() real ext-real Element of REAL
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),v) is Element of bool the carrier of ()
G00 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),G00) is Element of bool the carrier of ()
r is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,r) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,r)) `2 is V14() real ext-real Element of REAL
r + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB i) * (1,(r + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
((GoB i) * (1,(r + 1))) `2 is V14() real ext-real Element of REAL
r is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),r) is Element of bool the carrier of ()
v is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip ((GoB i),v) is Element of bool the carrier of ()
cell ((GoB i),G0,v) is Element of bool the carrier of ()
(v_strip ((GoB i),G0)) /\ (h_strip ((GoB i),v)) is Element of bool the carrier of ()
G00 is set
Y is set
x is set
p is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G0 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB i),p,G0) is Element of bool the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : i <= b2 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not b2 <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not i <= b2 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not i <= b1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : i <= b1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not b1 <= i } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= i } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not b2 <= i } is set
j is Element of bool the carrier of ()
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of ()
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : i <= b2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not i <= b2 } is set
j is Element of bool the carrier of ()
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of ()
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : i <= b1 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not i <= b1 } is set
j is Element of bool the carrier of ()
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of ()
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
i is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= i } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not b1 <= i } is set
j is Element of bool the carrier of ()
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
Y is set
x is V43(2) V100() FinSequence-like Element of the carrier of ()
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
|[(x `1),(x `2)]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
Y is set
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G0 is V14() real ext-real Element of REAL
u is V14() real ext-real Element of REAL
|[G0,u]| is V43(2) V100() FinSequence-like Element of the carrier of ()
the carrier of () \ G is Element of bool the carrier of ()
i is Element of bool the carrier of ()
j is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= j } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not b2 <= j } is set
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
i is Element of bool the carrier of ()
j is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : j <= b2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not j <= b2 } is set
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
i is Element of bool the carrier of ()
j is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= j } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not b1 <= j } is set
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
i is Element of bool the carrier of ()
j is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : j <= b1 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : not j <= b1 } is set
G is Element of bool the carrier of ()
G ` is Element of bool the carrier of ()
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
h_strip (j,i) is Element of bool the carrier of ()
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,i)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b2 } is set
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (j * (1,(i + 1))) `2 } is set
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,i)) `2 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b2 & b2 <= (j * (1,(i + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (j * (1,(i + 1))) `2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b2 } /\ { |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (j * (1,(i + 1))) `2 } is set
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
u is V14() real ext-real Element of REAL
v is V14() real ext-real Element of REAL
|[u,v]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
Y is Element of bool the carrier of ()
G is Element of bool the carrier of ()
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,i)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (1,i)) `2 <= b2 } is set
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
v_strip (j,i) is Element of bool the carrier of ()
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (i,1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b1 } is set
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (j * ((i + 1),1)) `1 } is set
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (i,1)) `1 is V14() real ext-real Element of REAL
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b1 & b1 <= (j * ((i + 1),1)) `1 ) } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (j * ((i + 1),1)) `1 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b1 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b1 } /\ { |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (j * ((i + 1),1)) `1 } is set
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G0 is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[G0,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
u is V14() real ext-real Element of REAL
v is V14() real ext-real Element of REAL
|[u,v]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is set
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
Y is Element of bool the carrier of ()
G is Element of bool the carrier of ()
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (i,1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (i,1)) `1 <= b1 } is set
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
v_strip (i,0) is Element of bool the carrier of ()
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (i * (1,1)) `1 } is set
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (i,(len i)) is Element of bool the carrier of ()
i * ((len i),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * ((len i),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (i * ((len i),1)) `1 <= b1 } is set
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (j,i) is Element of bool the carrier of ()
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (i,1)) `1 is V14() real ext-real Element of REAL
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b1 & b1 <= (j * ((i + 1),1)) `1 ) } is set
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
h_strip (i,0) is Element of bool the carrier of ()
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (i * (1,1)) `2 } is set
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (i,()) is Element of bool the carrier of ()
i * (1,()) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,())) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (i * (1,())) `2 <= b2 } is set
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular FinSequence of K295( the carrier of ())
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (j,i) is Element of bool the carrier of ()
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,i)) `2 is V14() real ext-real Element of REAL
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b2 & b2 <= (j * (1,(i + 1))) `2 ) } is set
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
cell (i,0,0) is Element of bool the carrier of ()
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,1)) `1 is V14() real ext-real Element of REAL
(i * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( b1 <= (i * (1,1)) `1 & b2 <= (i * (1,1)) `2 ) } is set
v_strip (i,0) is Element of bool the carrier of ()
h_strip (i,0) is Element of bool the carrier of ()
(v_strip (i,0)) /\ (h_strip (i,0)) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (i * (1,1)) `2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (i * (1,1)) `1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (i,0,()) is Element of bool the carrier of ()
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,1)) `1 is V14() real ext-real Element of REAL
i * (1,()) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,())) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( b1 <= (i * (1,1)) `1 & (i * (1,())) `2 <= b2 ) } is set
v_strip (i,0) is Element of bool the carrier of ()
h_strip (i,()) is Element of bool the carrier of ()
(v_strip (i,0)) /\ (h_strip (i,())) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (i * (1,())) `2 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (i * (1,1)) `1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,0,i) is Element of bool the carrier of ()
j * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,1)) `1 is V14() real ext-real Element of REAL
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,i)) `2 is V14() real ext-real Element of REAL
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( b1 <= (j * (1,1)) `1 & (j * (1,i)) `2 <= b2 & b2 <= (j * (1,(i + 1))) `2 ) } is set
v_strip (j,0) is Element of bool the carrier of ()
h_strip (j,i) is Element of bool the carrier of ()
(v_strip (j,0)) /\ (h_strip (j,i)) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b2 & b2 <= (j * (1,(i + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b1 <= (j * (1,1)) `1 } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (i,(len i),0) is Element of bool the carrier of ()
i * ((len i),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * ((len i),1)) `1 is V14() real ext-real Element of REAL
i * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (i * ((len i),1)) `1 <= b1 & b2 <= (i * (1,1)) `2 ) } is set
v_strip (i,(len i)) is Element of bool the carrier of ()
h_strip (i,0) is Element of bool the carrier of ()
(v_strip (i,(len i))) /\ (h_strip (i,0)) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (i * (1,1)) `2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (i * ((len i),1)) `1 <= b1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
len i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (i,(len i),()) is Element of bool the carrier of ()
i * ((len i),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * ((len i),1)) `1 is V14() real ext-real Element of REAL
i * (1,()) is V43(2) V100() FinSequence-like Element of the carrier of ()
(i * (1,())) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (i * ((len i),1)) `1 <= b1 & (i * (1,())) `2 <= b2 ) } is set
v_strip (i,(len i)) is Element of bool the carrier of ()
h_strip (i,()) is Element of bool the carrier of ()
(v_strip (i,(len i))) /\ (h_strip (i,())) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (i * (1,())) `2 <= b2 } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (i * ((len i),1)) `1 <= b1 } is set
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
x is V14() real ext-real Element of REAL
p is V14() real ext-real Element of REAL
|[x,p]| is V43(2) V100() FinSequence-like Element of the carrier of ()
j is set
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is V14() real ext-real Element of REAL
Y is V14() real ext-real Element of REAL
|[G,Y]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,(len j),i) is Element of bool the carrier of ()
j * ((len j),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * ((len j),1)) `1 is V14() real ext-real Element of REAL
j * (1,i) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,i)) `2 is V14() real ext-real Element of REAL
j * (1,(i + 1)) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,(i + 1))) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * ((len j),1)) `1 <= b1 & (j * (1,i)) `2 <= b2 & b2 <= (j * (1,(i + 1))) `2 ) } is set
v_strip (j,(len j)) is Element of bool the carrier of ()
h_strip (j,i) is Element of bool the carrier of ()
(v_strip (j,(len j))) /\ (h_strip (j,i)) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (1,i)) `2 <= b2 & b2 <= (j * (1,(i + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * ((len j),1)) `1 <= b1 } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,i,0) is Element of bool the carrier of ()
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (i,1)) `1 is V14() real ext-real Element of REAL
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
j * (1,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,1)) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b1 & b1 <= (j * ((i + 1),1)) `1 & b2 <= (j * (1,1)) `2 ) } is set
v_strip (j,i) is Element of bool the carrier of ()
h_strip (j,0) is Element of bool the carrier of ()
(v_strip (j,i)) /\ (h_strip (j,0)) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b1 & b1 <= (j * ((i + 1),1)) `1 ) } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : b2 <= (j * (1,1)) `2 } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
len j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (j,i,()) is Element of bool the carrier of ()
j * (i,1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (i,1)) `1 is V14() real ext-real Element of REAL
j * ((i + 1),1) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * ((i + 1),1)) `1 is V14() real ext-real Element of REAL
j * (1,()) is V43(2) V100() FinSequence-like Element of the carrier of ()
(j * (1,())) `2 is V14() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b1 & b1 <= (j * ((i + 1),1)) `1 & (j * (1,())) `2 <= b2 ) } is set
v_strip (j,i) is Element of bool the carrier of ()
h_strip (j,()) is Element of bool the carrier of ()
(v_strip (j,i)) /\ (h_strip (j,())) is Element of bool the carrier of ()
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : ( (j * (i,1)) `1 <= b1 & b1 <= (j * ((i + 1),1)) `1 ) } is set
{ |[b1,b2]| where b1, b2 is V14() real ext-real Element of REAL : (j * (1,())) `2 <= b2 } is set
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
p is V14() real ext-real Element of REAL
G0 is V14() real ext-real Element of REAL
|[p,G0]| is V43(2) V100() FinSequence-like Element of the carrier of ()
G is set
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
Y is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
|[Y,x]| is V43(2) V100() FinSequence-like Element of the carrier of ()
i is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
i + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
j + 1 is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
G is V19() V21() V22( NAT ) V23(K295( the carrier of ())) V24() FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K295( the carrier of ())
len G is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
width G is natural V14() real ext-real V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (G,i,j) is Element of bool the carrier of ()
G * (i,1) is V43(2)