REAL is V45() V46() V47() V51() V63() V64() V66() set
NAT is non empty V4() V5() V6() V45() V46() V47() V48() V49() V50() V51() V52() V61() V63() V67() V68() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
NAT is non empty V4() V5() V6() V45() V46() V47() V48() V49() V50() V51() V52() V61() V63() V67() V68() set
K6(NAT) is V52() set
K6(NAT) is V52() set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K6( the carrier of (TOP-REAL 2)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V52() set
K7(K7(NAT,NAT),NAT) is V52() set
K6(K7(K7(NAT,NAT),NAT)) is V52() set
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() functional ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() V67() V69( {} ) FinSequence-membered set
3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() functional ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() V67() V69( {} ) FinSequence-membered Element of NAT
Seg 1 is non empty V2() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V69(1) Element of K6(NAT)
len {} is empty V4() V5() V6() V8() V9() V10() V11() V12() functional ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() V67() V69( {} ) FinSequence-membered set
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
TOP-REAL f is non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct
the carrier of (TOP-REAL f) is non empty set
g is V13() V16( NAT ) V17( the carrier of (TOP-REAL f)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL f)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
g . 1 is set
L~ g is Element of K6( the carrier of (TOP-REAL f))
K6( the carrier of (TOP-REAL f)) is set
g /. 1 is V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
g . (len g) is set
g /. (len g) is V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (g,1) is Element of K6( the carrier of (TOP-REAL f))
{ (LSeg (g,b1)) where b1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g ) } is set
g /. (1 + 1) is V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
LSeg ((g /. 1),(g /. (1 + 1))) is Element of K6( the carrier of (TOP-REAL f))
{ (((1 - b1) * (g /. 1)) + (b1 * (g /. (1 + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
union { (LSeg (g,b1)) where b1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g ) } is set
(len g) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
((len g) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (g,((len g) -' 1)) is Element of K6( the carrier of (TOP-REAL f))
g /. ((len g) -' 1) is V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
g /. (((len g) -' 1) + 1) is V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
LSeg ((g /. ((len g) -' 1)),(g /. (((len g) -' 1) + 1))) is Element of K6( the carrier of (TOP-REAL f))
{ (((1 - b1) * (g /. ((len g) -' 1))) + (b1 * (g /. (((len g) -' 1) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f `1 is V11() V12() ext-real Element of REAL
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
g `1 is V11() V12() ext-real Element of REAL
f `2 is V11() V12() ext-real Element of REAL
g `2 is V11() V12() ext-real Element of REAL
p is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (f,g) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * f) + (b1 * g)) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
p `1 is V11() V12() ext-real Element of REAL
f `1 is V11() V12() ext-real Element of REAL
p `2 is V11() V12() ext-real Element of REAL
f `2 is V11() V12() ext-real Element of REAL
Y is V11() V12() ext-real Element of REAL
1 - Y is V11() V12() ext-real Element of REAL
(1 - Y) * f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
Y * g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
((1 - Y) * f) + (Y * g) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V11() V12() ext-real Element of REAL
1 - i is V11() V12() ext-real Element of REAL
(1 - i) * f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
i * g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
((1 - i) * f) + (i * g) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
((1 - i) * f) `1 is V11() V12() ext-real Element of REAL
(i * g) `1 is V11() V12() ext-real Element of REAL
(((1 - i) * f) `1) + ((i * g) `1) is V11() V12() ext-real Element of REAL
(1 - i) * (f `1) is V11() V12() ext-real Element of REAL
((1 - i) * (f `1)) + ((i * g) `1) is V11() V12() ext-real Element of REAL
i * (g `1) is V11() V12() ext-real Element of REAL
((1 - i) * (f `1)) + (i * (g `1)) is V11() V12() ext-real Element of REAL
((1 - Y) * f) `1 is V11() V12() ext-real Element of REAL
(Y * g) `1 is V11() V12() ext-real Element of REAL
(((1 - Y) * f) `1) + ((Y * g) `1) is V11() V12() ext-real Element of REAL
(1 - Y) * (f `1) is V11() V12() ext-real Element of REAL
((1 - Y) * (f `1)) + ((Y * g) `1) is V11() V12() ext-real Element of REAL
Y * (g `1) is V11() V12() ext-real Element of REAL
((1 - Y) * (f `1)) + (Y * (g `1)) is V11() V12() ext-real Element of REAL
((1 - i) * f) `2 is V11() V12() ext-real Element of REAL
(i * g) `2 is V11() V12() ext-real Element of REAL
(((1 - i) * f) `2) + ((i * g) `2) is V11() V12() ext-real Element of REAL
(1 - i) * (f `2) is V11() V12() ext-real Element of REAL
((1 - i) * (f `2)) + ((i * g) `2) is V11() V12() ext-real Element of REAL
i * (g `2) is V11() V12() ext-real Element of REAL
((1 - i) * (f `2)) + (i * (g `2)) is V11() V12() ext-real Element of REAL
((1 - Y) * f) `2 is V11() V12() ext-real Element of REAL
(Y * g) `2 is V11() V12() ext-real Element of REAL
(((1 - Y) * f) `2) + ((Y * g) `2) is V11() V12() ext-real Element of REAL
(1 - Y) * (f `2) is V11() V12() ext-real Element of REAL
((1 - Y) * (f `2)) + ((Y * g) `2) is V11() V12() ext-real Element of REAL
Y * (g `2) is V11() V12() ext-real Element of REAL
((1 - Y) * (f `2)) + (Y * (g `2)) is V11() V12() ext-real Element of REAL
f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f `1 is V11() V12() ext-real Element of REAL
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
g `1 is V11() V12() ext-real Element of REAL
f `2 is V11() V12() ext-real Element of REAL
g `2 is V11() V12() ext-real Element of REAL
p is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (p,f) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * p) + (b1 * f)) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (f,g) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * f) + (b1 * g)) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
p `1 is V11() V12() ext-real Element of REAL
f `1 is V11() V12() ext-real Element of REAL
p `2 is V11() V12() ext-real Element of REAL
f `2 is V11() V12() ext-real Element of REAL
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f | g is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
len (f | g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
len (f | g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
len (f | g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
len (f | g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one V52() FinSequence-like FinSubsequence-like special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
p | g is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one V52() FinSequence-like FinSubsequence-like special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) -' g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f /^ g is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (f /^ g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) - g is V11() V12() ext-real Element of REAL
p is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one V52() FinSequence-like FinSubsequence-like special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
p /^ g is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like one-to-one V52() FinSequence-like FinSubsequence-like special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
len (p /^ g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
mid (f,g,p) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(g + 1) - g is V11() V12() ext-real Element of REAL
p - g is V11() V12() ext-real set
p -' g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(p -' g) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(len f) - g is V11() V12() ext-real Element of REAL
((len f) - g) + 1 is V11() V12() ext-real Element of REAL
g -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) -' (g -' 1) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) - (g -' 1) is V11() V12() ext-real Element of REAL
g - 1 is V11() V12() ext-real Element of REAL
(len f) - (g - 1) is V11() V12() ext-real Element of REAL
f /^ (g -' 1) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(f /^ (g -' 1)) | ((p -' g) + 1) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(p + 1) - p is V11() V12() ext-real Element of REAL
g - p is V11() V12() ext-real set
g -' p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(g -' p) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(len f) - p is V11() V12() ext-real Element of REAL
((len f) - p) + 1 is V11() V12() ext-real Element of REAL
p -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) -' (p -' 1) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) - (p -' 1) is V11() V12() ext-real Element of REAL
p - 1 is V11() V12() ext-real Element of REAL
(len f) - (p - 1) is V11() V12() ext-real Element of REAL
f /^ (p -' 1) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(f /^ (p -' 1)) | ((g -' p) + 1) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev ((f /^ (p -' 1)) | ((g -' p) + 1)) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT : g in LSeg (f,b1) } is set
f is set
Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,Y) is Element of K6( the carrier of (TOP-REAL 2))
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (f,f) is Element of K6( the carrier of (TOP-REAL 2))
Y is non empty V45() V46() V47() V48() V49() V50() V61() V63() Element of K6(NAT)
min Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
Y is non empty V45() V46() V47() V48() V49() V50() V61() V63() Element of K6(NAT)
min Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
i is non empty V45() V46() V47() V48() V49() V50() V61() V63() Element of K6(NAT)
min i is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,p) is Element of K6( the carrier of (TOP-REAL 2))
L~ f is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT : g in LSeg (f,b1) } is set
f is non empty V45() V46() V47() V48() V49() V50() V61() V63() Element of K6(NAT)
min f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT : g in LSeg (f,b1) } is set
p is non empty V45() V46() V47() V48() V49() V50() V61() V63() Element of K6(NAT)
min p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,f) is Element of K6( the carrier of (TOP-REAL 2))
(f,g) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,f) is Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,(f,g)) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT : g in LSeg (f,b1) } is set
p is non empty V45() V46() V47() V48() V49() V50() V61() V63() Element of K6(NAT)
min p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,f) is Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg (f,1) is Element of K6( the carrier of (TOP-REAL 2))
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
L~ f is Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f /. 1 is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,(f /. 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (f,1) is Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(f,g) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
p is V4() V5() V6() V10() V11() V12() ext-real non negative V52() V67() set
f . p is set
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
f /. p is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f is V4() V5() V6() V10() V11() V12() ext-real non negative V52() V67() set
f + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
1 + 0 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,Y) is Element of K6( the carrier of (TOP-REAL 2))
L~ f is Element of K6( the carrier of (TOP-REAL 2))
LSeg (f,(f,g)) is Element of K6( the carrier of (TOP-REAL 2))
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(f,g) + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(LSeg (f,(f,g))) /\ (LSeg (f,Y)) is Element of K6( the carrier of (TOP-REAL 2))
f /. Y is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
{(f /. Y)} is non empty V2() V69(1) set
(LSeg (f,(f,g))) /\ (LSeg (f,Y)) is Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(f,g) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,p) is Element of K6( the carrier of (TOP-REAL 2))
L~ f is Element of K6( the carrier of (TOP-REAL 2))
LSeg (f,(f,g)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,(f,g))) /\ (LSeg (f,p)) is Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,g) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (f,p) is Element of K6( the carrier of (TOP-REAL 2))
f . p is set
(f,g) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
LSeg (f,(f,g)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,(f,g))) /\ (LSeg (f,p)) is Element of K6( the carrier of (TOP-REAL 2))
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(f,g) + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
f /. ((f,g) + 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
{(f /. ((f,g) + 1))} is non empty V2() V69(1) set
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f . 1 is set
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . (len f) is set
(Rev f) . 1 is set
len (Rev f) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(Rev f) . (len (Rev f)) is set
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
dom (Rev f) is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
(Rev f) . (len f) is set
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
g is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
p is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
<*p*> is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() V69(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
(f,p) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(f,p) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
mid (f,((f,p) + 1),(len f)) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*p*> ^ (mid (f,((f,p) + 1),(len f))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f is V4() V5() V6() V10() V11() V12() ext-real non negative V52() V67() set
f + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (g,f) is Element of K6( the carrier of (TOP-REAL 2))
(f,p) + f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
((f,p) + f) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,(((f,p) + f) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
len <*p*> is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
len (mid (f,((f,p) + 1),(len f))) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len <*p*>) + (len (mid (f,((f,p) + 1),(len f)))) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
1 + (len (mid (f,((f,p) + 1),(len f)))) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(f + 1) - 1 is V11() V12() ext-real Element of REAL
(1 + (len (mid (f,((f,p) + 1),(len f))))) - 1 is V11() V12() ext-real Element of REAL
f -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
1 - 1 is V11() V12() ext-real Element of REAL
((f,p) + f) - 1 is V11() V12() ext-real Element of REAL
f - 1 is V11() V12() ext-real Element of REAL
1 + (f - 1) is V11() V12() ext-real Element of REAL
(len <*p*>) + (f -' 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
Y + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (f,Y) is Element of K6( the carrier of (TOP-REAL 2))
((f,p) + 1) - (f,p) is V11() V12() ext-real Element of REAL
(len f) - (f,p) is V11() V12() ext-real Element of REAL
((len f) - (f,p)) - 1 is V11() V12() ext-real Element of REAL
(len f) -' ((f,p) + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) - ((f,p) + 1) is V11() V12() ext-real Element of REAL
0 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((len f) -' ((f,p) + 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((len f) - ((f,p) + 1)) + 1 is V11() V12() ext-real Element of REAL
1 + (((len f) - ((f,p) + 1)) + 1) is V11() V12() ext-real Element of REAL
1 + ((len f) - (f,p)) is V11() V12() ext-real Element of REAL
f + (f,p) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
((len f) - (f,p)) + (f,p) is V11() V12() ext-real Element of REAL
(((f,p) + f) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
g /. (f + 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
g . (f + 1) is set
(len <*p*>) + ((f + 1) - 1) is V11() V12() ext-real Element of REAL
(f + 1) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len <*p*>) + ((f + 1) -' 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
dom (mid (f,((f,p) + 1),(len f))) is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
(mid (f,((f,p) + 1),(len f))) . ((f + 1) -' 1) is set
((f + 1) -' 1) + ((f,p) + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((f + 1) -' 1) + ((f,p) + 1)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . ((((f + 1) -' 1) + ((f,p) + 1)) -' 1) is set
((f + 1) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((f + 1) -' 1) + 1) + (f,p) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((((f + 1) -' 1) + 1) + (f,p)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . (((((f + 1) -' 1) + 1) + (f,p)) -' 1) is set
(f + 1) + (f,p) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f + 1) + (f,p)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . (((f + 1) + (f,p)) -' 1) is set
((f,p) + f) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((f,p) + f) + 1) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . ((((f,p) + f) + 1) -' 1) is set
f . ((f,p) + f) is set
f . ((((f,p) + f) -' 1) + 1) is set
f /. ((((f,p) + f) -' 1) + 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,p) + (f - 1) is V11() V12() ext-real Element of REAL
((f,p) + (f - 1)) + 1 is V11() V12() ext-real Element of REAL
f /. (((f,p) + f) -' 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. (((f,p) + f) -' 1)),(f /. ((((f,p) + f) -' 1) + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (f /. (((f,p) + f) -' 1))) + (b1 * (f /. ((((f,p) + f) -' 1) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
g . f is set
(mid (f,((f,p) + 1),(len f))) . (f -' 1) is set
(f -' 1) + ((f,p) + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f -' 1) + ((f,p) + 1)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . (((f -' 1) + ((f,p) + 1)) -' 1) is set
(f -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f -' 1) + 1) + (f,p) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((f -' 1) + 1) + (f,p)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . ((((f -' 1) + 1) + (f,p)) -' 1) is set
f . (((f,p) + f) -' 1) is set
g /. f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((g /. f),(g /. (f + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (g /. f)) + (b1 * (g /. (f + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dom <*p*> is non empty V2() V45() V46() V47() V48() V49() V50() V61() V63() V69(1) Element of K6(NAT)
g . f is set
<*p*> . f is set
g /. f is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (f,(f,p)) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (p,(g /. (f + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * p) + (b1 * (g /. (f + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
g is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f /. (len f) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f,p) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(f,p) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
f . ((f,p) + 1) is set
<*p*> is non empty V2() V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() V69(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
mid (f,((f,p) + 1),(len f)) is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*p*> ^ (mid (f,((f,p) + 1),(len f))) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
len <*p*> is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
len (mid (f,((f,p) + 1),(len f))) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len <*p*>) + (len (mid (f,((f,p) + 1),(len f)))) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
1 + (len (mid (f,((f,p) + 1),(len f)))) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (f,f) is Element of K6( the carrier of (TOP-REAL 2))
1 + f is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
i is V4() V5() V6() V10() V11() V12() ext-real non negative V52() V67() set
Y is V4() V5() V6() V10() V11() V12() ext-real non negative V52() V67() set
Y + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (g,Y) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (g,i) is Element of K6( the carrier of (TOP-REAL 2))
0 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(LSeg (g,Y)) /\ (LSeg (g,i)) is Element of K6( the carrier of (TOP-REAL 2))
i + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(f,p) + i is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
((f,p) + i) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,(((f,p) + i) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(f,p) + Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
1 - 1 is V11() V12() ext-real Element of REAL
((f,p) + Y) - 1 is V11() V12() ext-real Element of REAL
((f,p) + Y) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(f,p) + (Y + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f,p) + i) - 1 is V11() V12() ext-real Element of REAL
((f,p) + Y) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((f,p) + Y) + 1) - 1 is V11() V12() ext-real Element of REAL
(((f,p) + Y) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (f,(((f,p) + Y) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,(((f,p) + Y) -' 1))) /\ (LSeg (f,(((f,p) + i) -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (g,Y)) /\ (LSeg (g,i)) is Element of K6( the carrier of (TOP-REAL 2))
i + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(LSeg (g,Y)) /\ (LSeg (g,i)) is Element of K6( the carrier of (TOP-REAL 2))
i + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
i + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f,p) + 1) - (f,p) is V11() V12() ext-real Element of REAL
(len f) - (f,p) is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() ext-real Element of REAL
((len f) - (f,p)) - 1 is V11() V12() ext-real Element of REAL
(len f) -' ((f,p) + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len f) - ((f,p) + 1) is V11() V12() ext-real Element of REAL
0 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((len f) -' ((f,p) + 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative V52() V67() set
Y + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (g,Y) is Element of K6( the carrier of (TOP-REAL 2))
Y + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
LSeg (g,(Y + 1)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (g,Y)) /\ (LSeg (g,(Y + 1))) is Element of K6( the carrier of (TOP-REAL 2))
g /. (Y + 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
{(g /. (Y + 1))} is non empty V2() V69(1) set
(Y + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(f,p) + Y is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
((f,p) + Y) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,(((f,p) + Y) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(f,p) + (Y + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f,p) + (Y + 1)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
LSeg (f,(((f,p) + (Y + 1)) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,(((f,p) + Y) -' 1))) /\ (LSeg (f,(((f,p) + (Y + 1)) -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((f,p) + Y) - 1 is V11() V12() ext-real Element of REAL
((Y + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
(1 + (len (mid (f,((f,p) + 1),(len f))))) - 1 is V11() V12() ext-real Element of REAL
(Y + 1) + (f,p) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((len f) - (f,p)) + (f,p) is V11() V12() ext-real Element of REAL
((f,p) + Y) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
Y - 1 is V11() V12() ext-real Element of REAL
(f,p) + (Y - 1) is V11() V12() ext-real Element of REAL
((f,p) + (Y - 1)) + 1 is V11() V12() ext-real Element of REAL
(((f,p) + Y) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((f,p) + Y) - 1) + (1 + 1) is V11() V12() ext-real Element of REAL
(((f,p) + Y) -' 1) + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
f /. ((((f,p) + Y) -' 1) + 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
{(f /. ((((f,p) + Y) -' 1) + 1))} is non empty V2() V69(1) set
LSeg (f,((((f,p) + Y) -' 1) + 1)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,(((f,p) + Y) -' 1))) /\ (LSeg (f,((((f,p) + Y) -' 1) + 1))) is Element of K6( the carrier of (TOP-REAL 2))
g . (Y + 1) is set
g /. ((Y + 1) + 1) is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((g /. (Y + 1)),(g /. ((Y + 1) + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (g /. (Y + 1))) + (b1 * (g /. ((Y + 1) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
g /. Y is V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((g /. Y),(g /. (Y + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (g /. Y)) + (b1 * (g /. (Y + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((g /. Y),(g /. (Y + 1)))) /\ (LSeg ((g /. (Y + 1)),(g /. ((Y + 1) + 1)))) is Element of K6( the carrier of (TOP-REAL 2))
(Y + 1) - 1 is V11() V12() ext-real Element of REAL
((Y + 1) - 1) + 1 is V11() V12() ext-real Element of REAL
(Y + 1) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
((Y + 1) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(len <*p*>) + ((Y + 1) -' 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
dom (mid (f,((f,p) + 1),(len f))) is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
(mid (f,((f,p) + 1),(len f))) . ((Y + 1) -' 1) is set
((Y + 1) -' 1) + ((f,p) + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((Y + 1) -' 1) + ((f,p) + 1)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . ((((Y + 1) -' 1) + ((f,p) + 1)) -' 1) is set
(((Y + 1) -' 1) + 1) + (f,p) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
((((Y + 1) -' 1) + 1) + (f,p)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . (((((Y + 1) -' 1) + 1) + (f,p)) -' 1) is set
((Y + 1) + (f,p)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . (((Y + 1) + (f,p)) -' 1) is set
(((f,p) + Y) + 1) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . ((((f,p) + Y) + 1) -' 1) is set
f . ((f,p) + Y) is set
f . ((((f,p) + Y) -' 1) + 1) is set
(((f,p) + Y) + 1) - 1 is V11() V12() ext-real Element of REAL
(((f,p) + Y) - 1) + 1 is V11() V12() ext-real Element of REAL
((len f) - ((f,p) + 1)) + 1 is V11() V12() ext-real Element of REAL
1 + (((len f) - ((f,p) + 1)) + 1) is V11() V12() ext-real Element of REAL
1 + ((len f) - (f,p)) is V11() V12() ext-real Element of REAL
(len g) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(len g) - 1 is V11() V12() ext-real Element of REAL
dom (mid (f,((f,p) + 1),(len f))) is V45() V46() V47() V48() V49() V50() V63() Element of K6(NAT)
(len f) -' (f,p) is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
(mid (f,((f,p) + 1),(len f))) . ((len f) -' (f,p)) is set
((len f) -' (f,p)) + ((f,p) + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() V67() Element of NAT
(((len f) -' (f,p)) + ((f,p) + 1)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() V67() Element of NAT
f . ((((