REAL is non empty V12() non finite V87() V88() V89() V93() set
NAT is non empty V12() V18() V19() V20() non finite cardinal limit_cardinal V87() V88() V89() V90() V91() V92() V93() Element of K19(REAL)
K19(REAL) is V12() non finite set
COMPLEX is non empty V12() non finite V87() V93() set
NAT is non empty V12() V18() V19() V20() non finite cardinal limit_cardinal V87() V88() V89() V90() V91() V92() V93() set
K19(NAT) is V12() non finite set
RAT is non empty V12() non finite V87() V88() V89() V90() V93() set
INT is non empty V12() non finite V87() V88() V89() V90() V91() V93() set
K19(NAT) is V12() non finite set
1 is non empty ext-real positive V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
K20(1,1) is finite set
K19(K20(1,1)) is finite V39() set
K20(K20(1,1),1) is finite set
K19(K20(K20(1,1),1)) is finite V39() set
K20(K20(1,1),REAL) is set
K19(K20(K20(1,1),REAL)) is set
K20(REAL,REAL) is V12() non finite set
K20(K20(REAL,REAL),REAL) is V12() non finite set
K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set
2 is non empty ext-real positive V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
K20(2,2) is finite set
K20(K20(2,2),REAL) is set
K19(K20(K20(2,2),REAL)) is set
K19(K20(REAL,REAL)) is V12() non finite set
TOP-REAL 2 is non empty TopSpace-like V128() V153() V154() V155() V156() V157() V158() V159() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
K269( the U1 of (TOP-REAL 2)) is functional non empty FinSequence-membered M11( the U1 of (TOP-REAL 2))
K19( the U1 of (TOP-REAL 2)) is set
K20(COMPLEX,COMPLEX) is V12() non finite set
K19(K20(COMPLEX,COMPLEX)) is V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V12() non finite set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set
K20(RAT,RAT) is V12() non finite set
K19(K20(RAT,RAT)) is V12() non finite set
K20(K20(RAT,RAT),RAT) is V12() non finite set
K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set
K20(INT,INT) is V12() non finite set
K19(K20(INT,INT)) is V12() non finite set
K20(K20(INT,INT),INT) is V12() non finite set
K19(K20(K20(INT,INT),INT)) is V12() non finite set
K20(NAT,NAT) is V12() non finite set
K20(K20(NAT,NAT),NAT) is V12() non finite set
K19(K20(K20(NAT,NAT),NAT)) is V12() non finite set
{} is functional empty V18() V19() V20() V22() V23() V24() V26() V33() finite V39() cardinal {} -element V87() V88() V89() V90() V91() V92() V93() FinSequence-membered set
3 is non empty ext-real positive V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
0 is functional empty ext-real V18() V19() V20() V22() V23() V24() V25() V26() V33() finite V39() cardinal {} -element V86() V87() V88() V89() V90() V91() V92() V93() FinSequence-membered Element of NAT
4 is non empty ext-real positive V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
1 / 2 is ext-real V25() V26() Element of REAL
p is ext-real V25() V26() Element of REAL
q is ext-real V25() V26() Element of REAL
p - q is ext-real V25() V26() Element of REAL
abs (p - q) is ext-real V25() V26() Element of REAL
p1 is ext-real V25() V26() Element of REAL
p + p1 is ext-real V25() V26() Element of REAL
q + p1 is ext-real V25() V26() Element of REAL
- (p - q) is ext-real V25() V26() Element of REAL
q - p is ext-real V25() V26() Element of REAL
p is ext-real V25() V26() Element of REAL
q is ext-real V25() V26() Element of REAL
p - q is ext-real V25() V26() Element of REAL
abs (p - q) is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
TOP-REAL p is non empty TopSpace-like V128() V153() V154() V155() V156() V157() V158() V159() strict RLTopStruct
the U1 of (TOP-REAL p) is non empty set
q is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
p1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q + p1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q1 + p1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
0. (TOP-REAL p) is p -element V51( TOP-REAL p) V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q + (0. (TOP-REAL p)) is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
p1 - p1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q + (p1 - p1) is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
(q + p1) - p1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q1 + (p1 - p1) is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q1 + (0. (TOP-REAL p)) is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
TOP-REAL p is non empty TopSpace-like V128() V153() V154() V155() V156() V157() V158() V159() strict RLTopStruct
the U1 of (TOP-REAL p) is non empty set
p1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
p1 + q is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
q1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
p1 + q1 is p -element V78() FinSequence-like Element of the U1 of (TOP-REAL p)
p is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p `1 is ext-real V25() V26() Element of REAL
q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
q `1 is ext-real V25() V26() Element of REAL
p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (q,p1) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * q) + (b1 * p1)) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 `1 is ext-real V25() V26() Element of REAL
q1 is ext-real V25() V26() Element of REAL
1 - q1 is ext-real V25() V26() Element of REAL
(1 - q1) * q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
q1 * p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - q1) * q) + (q1 * p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - q1) * q) `1 is ext-real V25() V26() Element of REAL
(q1 * p1) `1 is ext-real V25() V26() Element of REAL
(((1 - q1) * q) `1) + ((q1 * p1) `1) is ext-real V25() V26() Element of REAL
q1 * (p1 `1) is ext-real V25() V26() Element of REAL
(((1 - q1) * q) `1) + (q1 * (p1 `1)) is ext-real V25() V26() Element of REAL
(1 - q1) * (q `1) is ext-real V25() V26() Element of REAL
((1 - q1) * (q `1)) + (q1 * (p1 `1)) is ext-real V25() V26() Element of REAL
p is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p `2 is ext-real V25() V26() Element of REAL
q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
q `2 is ext-real V25() V26() Element of REAL
p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (q,p1) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * q) + (b1 * p1)) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 `2 is ext-real V25() V26() Element of REAL
q1 is ext-real V25() V26() Element of REAL
1 - q1 is ext-real V25() V26() Element of REAL
(1 - q1) * q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
q1 * p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - q1) * q) + (q1 * p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - q1) * q) `2 is ext-real V25() V26() Element of REAL
(q1 * p1) `2 is ext-real V25() V26() Element of REAL
(((1 - q1) * q) `2) + ((q1 * p1) `2) is ext-real V25() V26() Element of REAL
q1 * (p1 `2) is ext-real V25() V26() Element of REAL
(((1 - q1) * q) `2) + (q1 * (p1 `2)) is ext-real V25() V26() Element of REAL
(1 - q1) * (q `2) is ext-real V25() V26() Element of REAL
((1 - q1) * (q `2)) + (q1 * (p1 `2)) is ext-real V25() V26() Element of REAL
p is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p `1 is ext-real V25() V26() Element of REAL
p `2 is ext-real V25() V26() Element of REAL
q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
q `1 is ext-real V25() V26() Element of REAL
q `2 is ext-real V25() V26() Element of REAL
p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 `1 is ext-real V25() V26() Element of REAL
p1 `2 is ext-real V25() V26() Element of REAL
LSeg (p,p1) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * p) + (b1 * p1)) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[(p `1),(p `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
{p} is non empty V12() finite 1 -element set
{ b1 where b1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2) : ( b1 `1 = q `1 & p `2 <= b1 `2 & b1 `2 <= p1 `2 ) } is set
|[(q `1),(p `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
|[(q `1),(p1 `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
p is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p `1 is ext-real V25() V26() Element of REAL
p `2 is ext-real V25() V26() Element of REAL
q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
q `1 is ext-real V25() V26() Element of REAL
q `2 is ext-real V25() V26() Element of REAL
p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 `1 is ext-real V25() V26() Element of REAL
p1 `2 is ext-real V25() V26() Element of REAL
LSeg (p,p1) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * p) + (b1 * p1)) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[(p `1),(p `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
{p} is non empty V12() finite 1 -element set
{ b1 where b1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2) : ( b1 `2 = q `2 & p `1 <= b1 `1 & b1 `1 <= p1 `1 ) } is set
|[(p `1),(q `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(q `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * ((p + 1),(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,q)) + (p1 * ((p + 1),(q + 1))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * ((p1 * (p,q)) + (p1 * ((p + 1),(q + 1)))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * (p,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * ((p + 1),q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,(q + 1))) + (p1 * ((p + 1),q)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * ((p1 * (p,(q + 1))) + (p1 * ((p + 1),q))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),q)) `1 is ext-real V25() V26() Element of REAL
p1 * ((p + 1),1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),1)) `1 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),(q + 1))) `1 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `1 is ext-real V25() V26() Element of REAL
p1 * (p,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,1)) `1 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 1))) `1 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),(q + 1))) `2 is ext-real V25() V26() Element of REAL
p1 * (1,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,(q + 1))) `2 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 1))) `2 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `2 is ext-real V25() V26() Element of REAL
p1 * (1,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,q)) `2 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),q)) `2 is ext-real V25() V26() Element of REAL
((1 / 2) * ((p1 * (p,q)) + (p1 * ((p + 1),(q + 1))))) `2 is ext-real V25() V26() Element of REAL
((p1 * (p,q)) + (p1 * ((p + 1),(q + 1)))) `2 is ext-real V25() V26() Element of REAL
(1 / 2) * (((p1 * (p,q)) + (p1 * ((p + 1),(q + 1)))) `2) is ext-real V25() V26() Element of REAL
((p1 * (p,q)) `2) + ((p1 * ((p + 1),(q + 1))) `2) is ext-real V25() V26() Element of REAL
(1 / 2) * (((p1 * (p,q)) `2) + ((p1 * ((p + 1),(q + 1))) `2)) is ext-real V25() V26() Element of REAL
((p1 * (p,(q + 1))) + (p1 * ((p + 1),q))) `2 is ext-real V25() V26() Element of REAL
(1 / 2) * (((p1 * (p,(q + 1))) + (p1 * ((p + 1),q))) `2) is ext-real V25() V26() Element of REAL
((1 / 2) * ((p1 * (p,(q + 1))) + (p1 * ((p + 1),q)))) `2 is ext-real V25() V26() Element of REAL
((1 / 2) * ((p1 * (p,q)) + (p1 * ((p + 1),(q + 1))))) `1 is ext-real V25() V26() Element of REAL
((p1 * (p,q)) + (p1 * ((p + 1),(q + 1)))) `1 is ext-real V25() V26() Element of REAL
(1 / 2) * (((p1 * (p,q)) + (p1 * ((p + 1),(q + 1)))) `1) is ext-real V25() V26() Element of REAL
((p1 * (p,q)) `1) + ((p1 * ((p + 1),(q + 1))) `1) is ext-real V25() V26() Element of REAL
(1 / 2) * (((p1 * (p,q)) `1) + ((p1 * ((p + 1),(q + 1))) `1)) is ext-real V25() V26() Element of REAL
((p1 * (p,(q + 1))) + (p1 * ((p + 1),q))) `1 is ext-real V25() V26() Element of REAL
(1 / 2) * (((p1 * (p,(q + 1))) + (p1 * ((p + 1),q))) `1) is ext-real V25() V26() Element of REAL
((1 / 2) * ((p1 * (p,(q + 1))) + (p1 * ((p + 1),q)))) `1 is ext-real V25() V26() Element of REAL
|[(((1 / 2) * ((p1 * (p,(q + 1))) + (p1 * ((p + 1),q)))) `1),(((1 / 2) * ((p1 * (p,(q + 1))) + (p1 * ((p + 1),q)))) `2)]| is V1() V4( NAT ) Function-like non empty finite 2 -element V78() FinSequence-like FinSubsequence-like Element of the U1 of (TOP-REAL 2)
p is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
GoB p is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
width (GoB p) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
LSeg (p,q) is Element of K19( the U1 of (TOP-REAL 2))
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
dom p is finite V87() V88() V89() V90() V91() V92() Element of K19(NAT)
Indices (GoB p) is set
p /. q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
[p1,q1] is set
{p1,q1} is non empty finite V39() V87() V88() V89() V90() V91() V92() set
{p1} is non empty V12() finite V39() 1 -element V87() V88() V89() V90() V91() V92() set
{{p1,q1},{p1}} is non empty finite V39() set
(GoB p) * (p1,q1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB p) * (1,q1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (1,q1)) `2 is ext-real V25() V26() Element of REAL
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
x `2 is ext-real V25() V26() Element of REAL
len (GoB p) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
(p /. q) `2 is ext-real V25() V26() Element of REAL
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
(GoB p) * (1,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (1,1)) `2 is ext-real V25() V26() Element of REAL
p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 `2 is ext-real V25() V26() Element of REAL
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
GoB p is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB p) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
LSeg (p,q) is Element of K19( the U1 of (TOP-REAL 2))
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
dom p is finite V87() V88() V89() V90() V91() V92() Element of K19(NAT)
Indices (GoB p) is set
p /. q is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
[p1,q1] is set
{p1,q1} is non empty finite V39() V87() V88() V89() V90() V91() V92() set
{p1} is non empty V12() finite V39() 1 -element V87() V88() V89() V90() V91() V92() set
{{p1,q1},{p1}} is non empty finite V39() set
(GoB p) * (p1,q1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB p) * (p1,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (p1,1)) `1 is ext-real V25() V26() Element of REAL
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
x `1 is ext-real V25() V26() Element of REAL
width (GoB p) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
(p /. q) `1 is ext-real V25() V26() Element of REAL
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
(GoB p) * (1,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (1,1)) `1 is ext-real V25() V26() Element of REAL
p1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 `1 is ext-real V25() V26() Element of REAL
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
GoB p is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB p) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width (GoB p) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
L~ p is Element of K19( the U1 of (TOP-REAL 2))
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
cell ((GoB p),q,p1) is Element of K19( the U1 of (TOP-REAL 2))
Int (cell ((GoB p),q,p1)) is Element of K19( the U1 of (TOP-REAL 2))
v_strip ((GoB p),q) is Element of K19( the U1 of (TOP-REAL 2))
h_strip ((GoB p),p1) is Element of K19( the U1 of (TOP-REAL 2))
(v_strip ((GoB p),q)) /\ (h_strip ((GoB p),p1)) is Element of K19( the U1 of (TOP-REAL 2))
Int ((v_strip ((GoB p),q)) /\ (h_strip ((GoB p),p1))) is Element of K19( the U1 of (TOP-REAL 2))
Int (v_strip ((GoB p),q)) is Element of K19( the U1 of (TOP-REAL 2))
Int (h_strip ((GoB p),p1)) is Element of K19( the U1 of (TOP-REAL 2))
(Int (v_strip ((GoB p),q))) /\ (Int (h_strip ((GoB p),p1))) is Element of K19( the U1 of (TOP-REAL 2))
q1 is set
len p is non empty ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
{ (LSeg (p,b1)) where b1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
union { (LSeg (p,b1)) where b1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p ) } is set
x is set
r is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
LSeg (p,r) is Element of K19( the U1 of (TOP-REAL 2))
r + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
j1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
(GoB p) * (1,j1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (1,j1)) `2 is ext-real V25() V26() Element of REAL
p1 + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
i1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB p) * (1,p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (1,p1)) `2 is ext-real V25() V26() Element of REAL
i1 `2 is ext-real V25() V26() Element of REAL
i1 `2 is ext-real V25() V26() Element of REAL
(GoB p) * (1,(p1 + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (1,(p1 + 1))) `2 is ext-real V25() V26() Element of REAL
i1 `2 is ext-real V25() V26() Element of REAL
i1 `2 is ext-real V25() V26() Element of REAL
j1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
(GoB p) * (j1,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (j1,1)) `1 is ext-real V25() V26() Element of REAL
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
i1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB p) * (q,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * (q,1)) `1 is ext-real V25() V26() Element of REAL
i1 `1 is ext-real V25() V26() Element of REAL
i1 `1 is ext-real V25() V26() Element of REAL
(GoB p) * ((q + 1),1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB p) * ((q + 1),1)) `1 is ext-real V25() V26() Element of REAL
i1 `1 is ext-real V25() V26() Element of REAL
i1 `1 is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 2 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * (p,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,q)),(p1 * (p,(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,q))) + (b1 * (p1 * (p,(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 * (p,(q + 2)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,(q + 1))),(p1 * (p,(q + 2)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,(q + 1)))) + (b1 * (p1 * (p,(q + 2))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((p1 * (p,q)),(p1 * (p,(q + 1))))) /\ (LSeg ((p1 * (p,(q + 1))),(p1 * (p,(q + 2))))) is Element of K19( the U1 of (TOP-REAL 2))
{(p1 * (p,(q + 1)))} is non empty V12() finite 1 -element set
q1 is set
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,(q + 1))) `1 is ext-real V25() V26() Element of REAL
p1 * (p,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,1)) `1 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `1 is ext-real V25() V26() Element of REAL
x `1 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 1))) `2 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `2 is ext-real V25() V26() Element of REAL
x `2 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 2))) `2 is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 2 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * ((p + 1),q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,q)),(p1 * ((p + 1),q))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,q))) + (b1 * (p1 * ((p + 1),q)))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 * ((p + 2),q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * ((p + 1),q)),(p1 * ((p + 2),q))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * ((p + 1),q))) + (b1 * (p1 * ((p + 2),q)))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((p1 * (p,q)),(p1 * ((p + 1),q)))) /\ (LSeg ((p1 * ((p + 1),q)),(p1 * ((p + 2),q)))) is Element of K19( the U1 of (TOP-REAL 2))
{(p1 * ((p + 1),q))} is non empty V12() finite 1 -element set
q1 is set
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),q)) `2 is ext-real V25() V26() Element of REAL
p1 * (1,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,q)) `2 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `2 is ext-real V25() V26() Element of REAL
x `2 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),q)) `1 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `1 is ext-real V25() V26() Element of REAL
x `1 is ext-real V25() V26() Element of REAL
(p1 * ((p + 2),q)) `1 is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * (p,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,q)),(p1 * (p,(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,q))) + (b1 * (p1 * (p,(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 * ((p + 1),(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,(q + 1))),(p1 * ((p + 1),(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,(q + 1)))) + (b1 * (p1 * ((p + 1),(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((p1 * (p,q)),(p1 * (p,(q + 1))))) /\ (LSeg ((p1 * (p,(q + 1))),(p1 * ((p + 1),(q + 1))))) is Element of K19( the U1 of (TOP-REAL 2))
{(p1 * (p,(q + 1)))} is non empty V12() finite 1 -element set
q1 is set
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,(q + 1))) `2 is ext-real V25() V26() Element of REAL
p1 * (1,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,(q + 1))) `2 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),(q + 1))) `2 is ext-real V25() V26() Element of REAL
x `2 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `1 is ext-real V25() V26() Element of REAL
p1 * (p,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,1)) `1 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 1))) `1 is ext-real V25() V26() Element of REAL
x `1 is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * ((p + 1),(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,(q + 1))),(p1 * ((p + 1),(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,(q + 1)))) + (b1 * (p1 * ((p + 1),(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 * ((p + 1),q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * ((p + 1),q)),(p1 * ((p + 1),(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * ((p + 1),q))) + (b1 * (p1 * ((p + 1),(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((p1 * (p,(q + 1))),(p1 * ((p + 1),(q + 1))))) /\ (LSeg ((p1 * ((p + 1),q)),(p1 * ((p + 1),(q + 1))))) is Element of K19( the U1 of (TOP-REAL 2))
{(p1 * ((p + 1),(q + 1)))} is non empty V12() finite 1 -element set
q1 is set
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),q)) `1 is ext-real V25() V26() Element of REAL
p1 * ((p + 1),1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),1)) `1 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),(q + 1))) `1 is ext-real V25() V26() Element of REAL
x `1 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 1))) `2 is ext-real V25() V26() Element of REAL
p1 * (1,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,(q + 1))) `2 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),(q + 1))) `2 is ext-real V25() V26() Element of REAL
x `2 is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * ((p + 1),q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,q)),(p1 * ((p + 1),q))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,q))) + (b1 * (p1 * ((p + 1),q)))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 * (p,(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,q)),(p1 * (p,(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,q))) + (b1 * (p1 * (p,(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((p1 * (p,q)),(p1 * ((p + 1),q)))) /\ (LSeg ((p1 * (p,q)),(p1 * (p,(q + 1))))) is Element of K19( the U1 of (TOP-REAL 2))
{(p1 * (p,q))} is non empty V12() finite 1 -element set
q1 is set
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,q)) `1 is ext-real V25() V26() Element of REAL
p1 * (p,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (p,1)) `1 is ext-real V25() V26() Element of REAL
(p1 * (p,(q + 1))) `1 is ext-real V25() V26() Element of REAL
x `1 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `2 is ext-real V25() V26() Element of REAL
p1 * (1,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,q)) `2 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),q)) `2 is ext-real V25() V26() Element of REAL
x `2 is ext-real V25() V26() Element of REAL
p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 * (p,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p1 * ((p + 1),q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * (p,q)),(p1 * ((p + 1),q))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * (p,q))) + (b1 * (p1 * ((p + 1),q)))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 * ((p + 1),(q + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p1 * ((p + 1),q)),(p1 * ((p + 1),(q + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p1 * ((p + 1),q))) + (b1 * (p1 * ((p + 1),(q + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((p1 * (p,q)),(p1 * ((p + 1),q)))) /\ (LSeg ((p1 * ((p + 1),q)),(p1 * ((p + 1),(q + 1))))) is Element of K19( the U1 of (TOP-REAL 2))
{(p1 * ((p + 1),q))} is non empty V12() finite 1 -element set
q1 is set
x is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),q)) `1 is ext-real V25() V26() Element of REAL
p1 * ((p + 1),1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * ((p + 1),1)) `1 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),(q + 1))) `1 is ext-real V25() V26() Element of REAL
x `1 is ext-real V25() V26() Element of REAL
(p1 * (p,q)) `2 is ext-real V25() V26() Element of REAL
p1 * (1,q) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p1 * (1,q)) `2 is ext-real V25() V26() Element of REAL
(p1 * ((p + 1),q)) `2 is ext-real V25() V26() Element of REAL
x `2 is ext-real V25() V26() Element of REAL
p is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
x + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p * (q,p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p * (q,(p1 + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p * (q,p1)),(p * (q,(p1 + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p * (q,p1))) + (b1 * (p * (q,(p1 + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p * (q1,x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p * (q1,(x + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p * (q1,x)),(p * (q1,(x + 1)))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p * (q1,x))) + (b1 * (p * (q1,(x + 1))))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p1 - x is ext-real V25() V26() V33() Element of REAL
abs (p1 - x) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
r is set
i1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 is ext-real V25() V26() Element of REAL
1 - j1 is ext-real V25() V26() Element of REAL
(1 - j1) * (p * (q,p1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 * (p * (q,(p1 + 1))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - j1) * (p * (q,p1))) + (j1 * (p * (q,(p1 + 1)))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i2 is ext-real V25() V26() Element of REAL
1 - i2 is ext-real V25() V26() Element of REAL
(1 - i2) * (p * (q1,x)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i2 * (p * (q1,(x + 1))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - i2) * (p * (q1,x))) + (i2 * (p * (q1,(x + 1)))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q1,x)) `1 is ext-real V25() V26() Element of REAL
p * (q1,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q1,1)) `1 is ext-real V25() V26() Element of REAL
(p * (q1,(x + 1))) `1 is ext-real V25() V26() Element of REAL
(p * (q,p1)) `1 is ext-real V25() V26() Element of REAL
p * (q,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q,1)) `1 is ext-real V25() V26() Element of REAL
(p * (q,(p1 + 1))) `1 is ext-real V25() V26() Element of REAL
1 * ((p * (q,p1)) `1) is ext-real V25() V26() Element of REAL
(1 - j1) * ((p * (q,p1)) `1) is ext-real V25() V26() Element of REAL
j1 * ((p * (q,(p1 + 1))) `1) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,p1)) `1)) + (j1 * ((p * (q,(p1 + 1))) `1)) is ext-real V25() V26() Element of REAL
((1 - j1) * (p * (q,p1))) `1 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `1) + (j1 * ((p * (q,(p1 + 1))) `1)) is ext-real V25() V26() Element of REAL
(j1 * (p * (q,(p1 + 1)))) `1 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `1) + ((j1 * (p * (q,(p1 + 1)))) `1) is ext-real V25() V26() Element of REAL
i1 `1 is ext-real V25() V26() Element of REAL
((1 - i2) * (p * (q1,x))) `1 is ext-real V25() V26() Element of REAL
(i2 * (p * (q1,(x + 1)))) `1 is ext-real V25() V26() Element of REAL
(((1 - i2) * (p * (q1,x))) `1) + ((i2 * (p * (q1,(x + 1)))) `1) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q1,x)) `1) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,x)) `1)) + ((i2 * (p * (q1,(x + 1)))) `1) is ext-real V25() V26() Element of REAL
i2 * ((p * (q1,(x + 1))) `1) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,x)) `1)) + (i2 * ((p * (q1,(x + 1))) `1)) is ext-real V25() V26() Element of REAL
p * (q1,p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q1,p1)) `1 is ext-real V25() V26() Element of REAL
(p * (q1,(x + 1))) `2 is ext-real V25() V26() Element of REAL
p * (1,(x + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (1,(x + 1))) `2 is ext-real V25() V26() Element of REAL
p * (q,(x + 1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q,(x + 1))) `2 is ext-real V25() V26() Element of REAL
(p * (q1,x)) `2 is ext-real V25() V26() Element of REAL
p * (1,x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (1,x)) `2 is ext-real V25() V26() Element of REAL
p * (q,x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q,x)) `2 is ext-real V25() V26() Element of REAL
(p * (q,p1)) `2 is ext-real V25() V26() Element of REAL
(1 - j1) * ((p * (q,p1)) `2) is ext-real V25() V26() Element of REAL
(p * (q,(p1 + 1))) `2 is ext-real V25() V26() Element of REAL
j1 * ((p * (q,(p1 + 1))) `2) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,p1)) `2)) + (j1 * ((p * (q,(p1 + 1))) `2)) is ext-real V25() V26() Element of REAL
((1 - j1) * (p * (q,p1))) `2 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `2) + (j1 * ((p * (q,(p1 + 1))) `2)) is ext-real V25() V26() Element of REAL
(j1 * (p * (q,(p1 + 1)))) `2 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `2) + ((j1 * (p * (q,(p1 + 1)))) `2) is ext-real V25() V26() Element of REAL
i1 `2 is ext-real V25() V26() Element of REAL
((1 - i2) * (p * (q1,x))) `2 is ext-real V25() V26() Element of REAL
(i2 * (p * (q1,(x + 1)))) `2 is ext-real V25() V26() Element of REAL
(((1 - i2) * (p * (q1,x))) `2) + ((i2 * (p * (q1,(x + 1)))) `2) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q1,x)) `2) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,x)) `2)) + ((i2 * (p * (q1,(x + 1)))) `2) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q,x)) `2) is ext-real V25() V26() Element of REAL
i2 * ((p * (q,(x + 1))) `2) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q,x)) `2)) + (i2 * ((p * (q,(x + 1))) `2)) is ext-real V25() V26() Element of REAL
i2 * ((p * (q,x)) `2) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q,x)) `2)) + (i2 * ((p * (q,x)) `2)) is ext-real V25() V26() Element of REAL
1 * ((p * (q,x)) `2) is ext-real V25() V26() Element of REAL
(1 - j1) * ((p * (q,(p1 + 1))) `2) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,(p1 + 1))) `2)) + (j1 * ((p * (q,(p1 + 1))) `2)) is ext-real V25() V26() Element of REAL
1 * ((p * (q,(p1 + 1))) `2) is ext-real V25() V26() Element of REAL
j1 * ((p * (q,p1)) `2) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,p1)) `2)) + (j1 * ((p * (q,p1)) `2)) is ext-real V25() V26() Element of REAL
1 * ((p * (q,p1)) `2) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q,(x + 1))) `2) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q,(x + 1))) `2)) + (i2 * ((p * (q,(x + 1))) `2)) is ext-real V25() V26() Element of REAL
1 * ((p * (q,(x + 1))) `2) is ext-real V25() V26() Element of REAL
p is V1() non empty-yielding V4( NAT ) V5(K269( the U1 of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
width p is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
q1 + 1 is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
p * (q,p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p * ((q + 1),p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p * (q,p1)),(p * ((q + 1),p1))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p * (q,p1))) + (b1 * (p * ((q + 1),p1)))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p * (q1,x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
p * ((q1 + 1),x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((p * (q1,x)),(p * ((q1 + 1),x))) is Element of K19( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (p * (q1,x))) + (b1 * (p * ((q1 + 1),x)))) where b1 is ext-real V25() V26() Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
q - q1 is ext-real V25() V26() V33() Element of REAL
abs (q - q1) is ext-real V18() V19() V20() V24() V25() V26() V33() finite cardinal V86() V87() V88() V89() V90() V91() V92() Element of NAT
r is set
i1 is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 is ext-real V25() V26() Element of REAL
1 - j1 is ext-real V25() V26() Element of REAL
(1 - j1) * (p * (q,p1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 * (p * ((q + 1),p1)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - j1) * (p * (q,p1))) + (j1 * (p * ((q + 1),p1))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i2 is ext-real V25() V26() Element of REAL
1 - i2 is ext-real V25() V26() Element of REAL
(1 - i2) * (p * (q1,x)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i2 * (p * ((q1 + 1),x)) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 - i2) * (p * (q1,x))) + (i2 * (p * ((q1 + 1),x))) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q1,x)) `2 is ext-real V25() V26() Element of REAL
p * (1,x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (1,x)) `2 is ext-real V25() V26() Element of REAL
(p * ((q1 + 1),x)) `2 is ext-real V25() V26() Element of REAL
(p * (q,p1)) `2 is ext-real V25() V26() Element of REAL
p * (1,p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (1,p1)) `2 is ext-real V25() V26() Element of REAL
(p * ((q + 1),p1)) `2 is ext-real V25() V26() Element of REAL
1 * ((p * (q,p1)) `2) is ext-real V25() V26() Element of REAL
(1 - j1) * ((p * (q,p1)) `2) is ext-real V25() V26() Element of REAL
j1 * ((p * ((q + 1),p1)) `2) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,p1)) `2)) + (j1 * ((p * ((q + 1),p1)) `2)) is ext-real V25() V26() Element of REAL
((1 - j1) * (p * (q,p1))) `2 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `2) + (j1 * ((p * ((q + 1),p1)) `2)) is ext-real V25() V26() Element of REAL
(j1 * (p * ((q + 1),p1))) `2 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `2) + ((j1 * (p * ((q + 1),p1))) `2) is ext-real V25() V26() Element of REAL
i1 `2 is ext-real V25() V26() Element of REAL
((1 - i2) * (p * (q1,x))) `2 is ext-real V25() V26() Element of REAL
(i2 * (p * ((q1 + 1),x))) `2 is ext-real V25() V26() Element of REAL
(((1 - i2) * (p * (q1,x))) `2) + ((i2 * (p * ((q1 + 1),x))) `2) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q1,x)) `2) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,x)) `2)) + ((i2 * (p * ((q1 + 1),x))) `2) is ext-real V25() V26() Element of REAL
i2 * ((p * ((q1 + 1),x)) `2) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,x)) `2)) + (i2 * ((p * ((q1 + 1),x)) `2)) is ext-real V25() V26() Element of REAL
p * (q,x) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q,x)) `2 is ext-real V25() V26() Element of REAL
(p * ((q1 + 1),x)) `1 is ext-real V25() V26() Element of REAL
p * ((q1 + 1),1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * ((q1 + 1),1)) `1 is ext-real V25() V26() Element of REAL
p * ((q1 + 1),p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * ((q1 + 1),p1)) `1 is ext-real V25() V26() Element of REAL
(p * (q1,x)) `1 is ext-real V25() V26() Element of REAL
p * (q1,1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q1,1)) `1 is ext-real V25() V26() Element of REAL
p * (q1,p1) is 2 -element V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(p * (q1,p1)) `1 is ext-real V25() V26() Element of REAL
(p * (q,p1)) `1 is ext-real V25() V26() Element of REAL
(1 - j1) * ((p * (q,p1)) `1) is ext-real V25() V26() Element of REAL
(p * ((q + 1),p1)) `1 is ext-real V25() V26() Element of REAL
j1 * ((p * ((q + 1),p1)) `1) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,p1)) `1)) + (j1 * ((p * ((q + 1),p1)) `1)) is ext-real V25() V26() Element of REAL
((1 - j1) * (p * (q,p1))) `1 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `1) + (j1 * ((p * ((q + 1),p1)) `1)) is ext-real V25() V26() Element of REAL
(j1 * (p * ((q + 1),p1))) `1 is ext-real V25() V26() Element of REAL
(((1 - j1) * (p * (q,p1))) `1) + ((j1 * (p * ((q + 1),p1))) `1) is ext-real V25() V26() Element of REAL
i1 `1 is ext-real V25() V26() Element of REAL
((1 - i2) * (p * (q1,x))) `1 is ext-real V25() V26() Element of REAL
(i2 * (p * ((q1 + 1),x))) `1 is ext-real V25() V26() Element of REAL
(((1 - i2) * (p * (q1,x))) `1) + ((i2 * (p * ((q1 + 1),x))) `1) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q1,x)) `1) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,x)) `1)) + ((i2 * (p * ((q1 + 1),x))) `1) is ext-real V25() V26() Element of REAL
(1 - i2) * ((p * (q1,p1)) `1) is ext-real V25() V26() Element of REAL
i2 * ((p * ((q1 + 1),p1)) `1) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,p1)) `1)) + (i2 * ((p * ((q1 + 1),p1)) `1)) is ext-real V25() V26() Element of REAL
i2 * ((p * (q1,p1)) `1) is ext-real V25() V26() Element of REAL
((1 - i2) * ((p * (q1,p1)) `1)) + (i2 * ((p * (q1,p1)) `1)) is ext-real V25() V26() Element of REAL
1 * ((p * (q1,p1)) `1) is ext-real V25() V26() Element of REAL
(1 - j1) * ((p * ((q + 1),p1)) `1) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * ((q + 1),p1)) `1)) + (j1 * ((p * ((q + 1),p1)) `1)) is ext-real V25() V26() Element of REAL
1 * ((p * ((q + 1),p1)) `1) is ext-real V25() V26() Element of REAL
j1 * ((p * (q,p1)) `1) is ext-real V25() V26() Element of REAL
((1 - j1) * ((p * (q,p1)) `1)) + (j1 * ((p * (q,p1)) `1)) is