:: ALGSTR_3 semantic presentation

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

c

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) + c

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

c

(x9 * z) + c

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

c

aa9 - c

(aa9 - c

x9 * ((aa9 - c

c

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 - c

- (((aa9 - c

(- (((aa9 - c

(((aa9 - c

((aa9 - c

- (x9 * ((aa9 - c

(- (x9 * ((aa9 - c

(((aa9 - c

((aa9 - c

(((aa9 - c

(aa9 - c

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

c

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) + c

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

c

uu * c

(uu * c

uu9 * c

(uu9 * c

c

uu * (c

uu9 * (c

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

c

(F,z,a,c

the of F . (z,a,c

(F,z,x,c

the of F . (z,x,c

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