REAL is non empty V13() V14() V15() V19() V37() set
NAT is V13() V14() V15() V16() V17() V18() V19() Element of K6(REAL)
K6(REAL) is set
NAT is V13() V14() V15() V16() V17() V18() V19() set
K6(NAT) is set
K6(NAT) is set
{} is set
1 is non empty V10() V11() V12() V13() V14() V15() V16() V17() V18() Element of NAT
0 is V10() V11() V12() V13() V14() V15() V16() V17() V18() Element of NAT
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
K8( the non empty set , the non empty set , the non empty set ) is set
K7(K8( the non empty set , the non empty set , the non empty set ), the non empty set ) is set
K6(K7(K8( the non empty set , the non empty set , the non empty set ), the non empty set )) is set
the V25() V34(K8( the non empty set , the non empty set , the non empty set ), the non empty set ) Element of K6(K7(K8( the non empty set , the non empty set , the non empty set ), the non empty set )) is V25() V34(K8( the non empty set , the non empty set , the non empty set ), the non empty set ) Element of K6(K7(K8( the non empty set , the non empty set , the non empty set ), the non empty set ))
( the non empty set , the Element of the non empty set , the Element of the non empty set , the V25() V34(K8( the non empty set , the non empty set , the non empty set ), the non empty set ) Element of K6(K7(K8( the non empty set , the non empty set , the non empty set ), the non empty set ))) is () ()
the carrier of ( the non empty set , the Element of the non empty set , the Element of the non empty set , the V25() V34(K8( the non empty set , the non empty set , the non empty set ), the non empty set ) Element of K6(K7(K8( the non empty set , the non empty set , the non empty set ), the non empty set ))) is set
F is non empty ()
the carrier of F is non empty set
the of F is V25() V34(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) Element of K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F))
K8( the carrier of F, the carrier of F, the carrier of F) is set
K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) is set
K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F)) is set
a is Element of the carrier of F
x is Element of the carrier of F
b is Element of the carrier of F
the of F . (a,x,b) is Element of the carrier of F
K8(REAL,REAL,REAL) is set
K7(K8(REAL,REAL,REAL),REAL) is set
K6(K7(K8(REAL,REAL,REAL),REAL)) is set
F is V25() V34(K8(REAL,REAL,REAL), REAL ) Element of K6(K7(K8(REAL,REAL,REAL),REAL))
F is V25() V34(K8(REAL,REAL,REAL), REAL ) Element of K6(K7(K8(REAL,REAL,REAL),REAL))
a is V25() V34(K8(REAL,REAL,REAL), REAL ) Element of K6(K7(K8(REAL,REAL,REAL),REAL))
x is V11() V12() Element of REAL
b is V11() V12() Element of REAL
x9 is V11() V12() Element of REAL
F . (x,b,x9) is V11() V12() Element of REAL
a . (x,b,x9) is V11() V12() Element of REAL
x * b is V11() V12() Element of REAL
(x * b) + x9 is V11() V12() Element of REAL
() is V25() V34(K8(REAL,REAL,REAL), REAL ) Element of K6(K7(K8(REAL,REAL,REAL),REAL))
(REAL,0,1,()) is () ()
() is () ()
the carrier of () is non empty set
the of () is V25() V34(K8( the carrier of (), the carrier of (), the carrier of ()), the carrier of ()) Element of K6(K7(K8( the carrier of (), the carrier of (), the carrier of ()), the carrier of ()))
K8( the carrier of (), the carrier of (), the carrier of ()) is set
K7(K8( the carrier of (), the carrier of (), the carrier of ()), the carrier of ()) is set
K6(K7(K8( the carrier of (), the carrier of (), the carrier of ()), the carrier of ())) is set
F is Element of the carrier of ()
a is Element of the carrier of ()
x is Element of the carrier of ()
the of () . (F,a,x) is Element of the carrier of ()
F is V11() V12() Element of REAL
a is V11() V12() Element of REAL
x is V11() V12() Element of REAL
b is V11() V12() Element of REAL
b - x is V11() V12() Element of REAL
F - a is V11() V12() Element of REAL
(b - x) / (F - a) is V11() V12() Element of REAL
(F - a) * ((b - x) / (F - a)) is V11() V12() Element of REAL
z is V11() V12() Element of REAL
F * z is V11() V12() Element of REAL
(F * z) + x is V11() V12() Element of REAL
a * z is V11() V12() Element of REAL
(a * z) + b is V11() V12() Element of REAL
F is Element of the carrier of ()
b is V11() V12() Element of REAL
a is Element of the carrier of ()
x9 is V11() V12() Element of REAL
x is Element of the carrier of ()
z is V11() V12() Element of REAL
((),F,a,x) is Element of the carrier of ()
the of () . (F,a,x) is Element of the carrier of ()
b * x9 is V11() V12() Element of REAL
(b * x9) + z is V11() V12() Element of REAL
1. () is Element of the carrier of ()
the OneF of () is Element of the carrier of ()
0. () is V56(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
F is Element of the carrier of ()
((),F,(1. ()),(0. ())) is Element of the carrier of ()
the of () . (F,(1. ()),(0. ())) is Element of the carrier of ()
a is V11() V12() Element of REAL
a * 1 is V11() V12() Element of REAL
(a * 1) + 0 is V11() V12() Element of REAL
F is Element of the carrier of ()
((),(1. ()),F,(0. ())) is Element of the carrier of ()
the of () . ((1. ()),F,(0. ())) is Element of the carrier of ()
a is V11() V12() Element of REAL
a * 1 is V11() V12() Element of REAL
(a * 1) + 0 is V11() V12() Element of REAL
F is Element of the carrier of ()
a is Element of the carrier of ()
((),F,(0. ()),a) is Element of the carrier of ()
the of () . (F,(0. ()),a) is Element of the carrier of ()
x is V11() V12() Element of REAL
x * 0 is V11() V12() Element of REAL
b is V11() V12() Element of REAL
(x * 0) + b is V11() V12() Element of REAL
F is Element of the carrier of ()
a is Element of the carrier of ()
((),(0. ()),F,a) is Element of the carrier of ()
the of () . ((0. ()),F,a) is Element of the carrier of ()
x is V11() V12() Element of REAL
0 * x is V11() V12() Element of REAL
b is V11() V12() Element of REAL
(0 * x) + b is V11() V12() Element of REAL
F is Element of the carrier of ()
a is Element of the carrier of ()
x is Element of the carrier of ()
z is V11() V12() Element of REAL
b is V11() V12() Element of REAL
x9 is V11() V12() Element of REAL
b * x9 is V11() V12() Element of REAL
z - (b * x9) is V11() V12() Element of REAL
c7 is V11() V12() Element of REAL
aa9 is Element of the carrier of ()
((),F,a,aa9) is Element of the carrier of ()
the of () . (F,a,aa9) is Element of the carrier of ()
(b * x9) + c7 is V11() V12() Element of REAL
F is Element of the carrier of ()
a is Element of the carrier of ()
x is Element of the carrier of ()
((),F,a,x) is Element of the carrier of ()
the of () . (F,a,x) is Element of the carrier of ()
b is Element of the carrier of ()
((),F,a,b) is Element of the carrier of ()
the of () . (F,a,b) is Element of the carrier of ()
x9 is V11() V12() Element of REAL
z is V11() V12() Element of REAL
x9 * z is V11() V12() Element of REAL
c7 is V11() V12() Element of REAL
(x9 * z) + c7 is V11() V12() Element of REAL
aa9 is V11() V12() Element of REAL
(x9 * z) + aa9 is V11() V12() Element of REAL
F is Element of the carrier of ()
a is Element of the carrier of ()
x is Element of the carrier of ()
b is Element of the carrier of ()
z is V11() V12() Element of REAL
x9 is V11() V12() Element of REAL
z - x9 is V11() V12() Element of REAL
aa9 is V11() V12() Element of REAL
c7 is V11() V12() Element of REAL
aa9 - c7 is V11() V12() Element of REAL
(aa9 - c7) / (z - x9) is V11() V12() Element of REAL
x9 * ((aa9 - c7) / (z - x9)) is V11() V12() Element of REAL
c7 - (x9 * ((aa9 - c7) / (z - x9))) is V11() V12() Element of REAL
vv is Element of the carrier of ()
vv9 is Element of the carrier of ()
((),vv,F,vv9) is Element of the carrier of ()
the of () . (vv,F,vv9) is Element of the carrier of ()
((),vv,a,vv9) is Element of the carrier of ()
the of () . (vv,a,vv9) is Element of the carrier of ()
((aa9 - c7) / (z - x9)) * x9 is V11() V12() Element of REAL
- (((aa9 - c7) / (z - x9)) * x9) is V11() V12() Element of REAL
(- (((aa9 - c7) / (z - x9)) * x9)) + c7 is V11() V12() Element of REAL
(((aa9 - c7) / (z - x9)) * x9) + ((- (((aa9 - c7) / (z - x9)) * x9)) + c7) is V11() V12() Element of REAL
((aa9 - c7) / (z - x9)) * z is V11() V12() Element of REAL
- (x9 * ((aa9 - c7) / (z - x9))) is V11() V12() Element of REAL
(- (x9 * ((aa9 - c7) / (z - x9)))) + c7 is V11() V12() Element of REAL
(((aa9 - c7) / (z - x9)) * z) + ((- (x9 * ((aa9 - c7) / (z - x9)))) + c7) is V11() V12() Element of REAL
((aa9 - c7) / (z - x9)) * (z - x9) is V11() V12() Element of REAL
(((aa9 - c7) / (z - x9)) * (z - x9)) + c7 is V11() V12() Element of REAL
(aa9 - c7) + c7 is V11() V12() Element of REAL
F is Element of the carrier of ()
a is Element of the carrier of ()
x is Element of the carrier of ()
b is Element of the carrier of ()
x9 is V11() V12() Element of REAL
c7 is V11() V12() Element of REAL
z is V11() V12() Element of REAL
aa9 is V11() V12() Element of REAL
uu is V11() V12() Element of REAL
x9 * uu is V11() V12() Element of REAL
(x9 * uu) + c7 is V11() V12() Element of REAL
z * uu is V11() V12() Element of REAL
(z * uu) + aa9 is V11() V12() Element of REAL
uu9 is Element of the carrier of ()
((),F,uu9,x) is Element of the carrier of ()
the of () . (F,uu9,x) is Element of the carrier of ()
((),a,uu9,b) is Element of the carrier of ()
the of () . (a,uu9,b) is Element of the carrier of ()
x is Element of the carrier of ()
F is Element of the carrier of ()
x9 is Element of the carrier of ()
((),x,F,x9) is Element of the carrier of ()
the of () . (x,F,x9) is Element of the carrier of ()
b is Element of the carrier of ()
z is Element of the carrier of ()
((),b,F,z) is Element of the carrier of ()
the of () . (b,F,z) is Element of the carrier of ()
a is Element of the carrier of ()
((),x,a,x9) is Element of the carrier of ()
the of () . (x,a,x9) is Element of the carrier of ()
((),b,a,z) is Element of the carrier of ()
the of () . (b,a,z) is Element of the carrier of ()
uu is V11() V12() Element of REAL
aa9 is V11() V12() Element of REAL
uu * aa9 is V11() V12() Element of REAL
vv is V11() V12() Element of REAL
(uu * aa9) + vv is V11() V12() Element of REAL
uu9 is V11() V12() Element of REAL
uu9 * aa9 is V11() V12() Element of REAL
vv9 is V11() V12() Element of REAL
(uu9 * aa9) + vv9 is V11() V12() Element of REAL
c7 is V11() V12() Element of REAL
uu * c7 is V11() V12() Element of REAL
(uu * c7) + vv is V11() V12() Element of REAL
uu9 * c7 is V11() V12() Element of REAL
(uu9 * c7) + vv9 is V11() V12() Element of REAL
c7 - aa9 is V11() V12() Element of REAL
uu * (c7 - aa9) is V11() V12() Element of REAL
uu9 * (c7 - aa9) is V11() V12() Element of REAL
F is non empty () ()
the carrier of F is non empty set
a is Element of the carrier of F
x is Element of the carrier of F
b is Element of the carrier of F
x9 is Element of the carrier of F
(F,b,a,x9) is Element of the carrier of F
the of F is V25() V34(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) Element of K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F))
K8( the carrier of F, the carrier of F, the carrier of F) is set
K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) is set
K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F)) is set
the of F . (b,a,x9) is Element of the carrier of F
(F,b,x,x9) is Element of the carrier of F
the of F . (b,x,x9) is Element of the carrier of F
z is Element of the carrier of F
c7 is Element of the carrier of F
(F,z,a,c7) is Element of the carrier of F
the of F . (z,a,c7) is Element of the carrier of F
(F,z,x,c7) is Element of the carrier of F
the of F . (z,x,c7) is Element of the carrier of F
F is non empty () ()
the carrier of F is non empty set
0. F is V56(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a is Element of the carrier of F
x is Element of the carrier of F
b is Element of the carrier of F
x9 is Element of the carrier of F
(F,a,x9,x) is Element of the carrier of F
the of F is V25() V34(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) Element of K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F))
K8( the carrier of F, the carrier of F, the carrier of F) is set
K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) is set
K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F)) is set
the of F . (a,x9,x) is Element of the carrier of F
(F,(0. F),x9,b) is Element of the carrier of F
the of F . ((0. F),x9,b) is Element of the carrier of F
F is non empty () ()
the carrier of F is non empty set
0. F is V56(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a is Element of the carrier of F
x is Element of the carrier of F
b is Element of the carrier of F
(F,a,x,b) is Element of the carrier of F
the of F is V25() V34(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) Element of K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F))
K8( the carrier of F, the carrier of F, the carrier of F) is set
K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) is set
K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F)) is set
the of F . (a,x,b) is Element of the carrier of F
x9 is Element of the carrier of F
(F,a,x9,b) is Element of the carrier of F
the of F . (a,x9,b) is Element of the carrier of F
(F,(0. F),x,(F,a,x,b)) is Element of the carrier of F
the of F . ((0. F),x,(F,a,x,b)) is Element of the carrier of F
(F,(0. F),x9,(F,a,x,b)) is Element of the carrier of F
the of F . ((0. F),x9,(F,a,x,b)) is Element of the carrier of F
F is non empty () ()
the carrier of F is non empty set
0. F is V56(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a is Element of the carrier of F
x is Element of the carrier of F
b is Element of the carrier of F
x9 is Element of the carrier of F
z is Element of the carrier of F
(F,x9,a,z) is Element of the carrier of F
the of F is V25() V34(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) Element of K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F))
K8( the carrier of F, the carrier of F, the carrier of F) is set
K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) is set
K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F)) is set
the of F . (x9,a,z) is Element of the carrier of F
(F,x9,(0. F),z) is Element of the carrier of F
the of F . (x9,(0. F),z) is Element of the carrier of F
(F,x9,a,x) is Element of the carrier of F
the of F . (x9,a,x) is Element of the carrier of F
F is non empty () ()
the carrier of F is non empty set
0. F is V56(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a is Element of the carrier of F
x is Element of the carrier of F
b is Element of the carrier of F
(F,x,a,b) is Element of the carrier of F
the of F is V25() V34(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) Element of K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F))
K8( the carrier of F, the carrier of F, the carrier of F) is set
K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F) is set
K6(K7(K8( the carrier of F, the carrier of F, the carrier of F), the carrier of F)) is set
the of F . (x,a,b) is Element of the carrier of F
x9 is Element of the carrier of F
(F,x9,a,b) is Element of the carrier of F
the of F . (x9,a,b) is Element of the carrier of F
(F,x,(0. F),b) is Element of the carrier of F
the of F . (x,(0. F),b) is Element of the carrier of F
(F,x9,(0. F),b) is Element of the carrier of F
the of F . (x9,(0. F),b) is Element of the carrier of F