:: SIN_COS2 semantic presentation

REAL is non empty V52() V53() V54() V58() V66() set
NAT is V52() V53() V54() V55() V56() V57() V58() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V52() V58() V66() set
RAT is non empty V52() V53() V54() V55() V58() V66() set
INT is non empty V52() V53() V54() V55() V56() V58() V66() set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
{} is empty V52() V53() V54() V55() V56() V57() V58() set
1 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
{{},1} is non empty set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
omega is V52() V53() V54() V55() V56() V57() V58() set
K19(omega) is set
K19(NAT) is set
0 is empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() Element of NAT
sqrt 1 is V30() real ext-real Element of REAL
{0} is non empty V52() V53() V54() V55() V56() V57() set
sin is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom sin is V52() V53() V54() Element of K19(REAL)
cos is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom cos is V52() V53() V54() Element of K19(REAL)
exp_R is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom exp_R is V52() V53() V54() Element of K19(REAL)
exp_R 0 is V30() real ext-real Element of REAL
2 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
PI is V30() real ext-real Element of REAL
2 * PI is V30() real ext-real Element of REAL
PI / 2 is V30() real ext-real Element of REAL
].0,(PI / 2).[ is open V52() V53() V54() Element of K19(REAL)
compreal is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real set
ff is V30() real ext-real set
p * ff is V30() real ext-real Element of REAL
sqrt (p * ff) is V30() real ext-real Element of REAL
2 * (sqrt (p * ff)) is V30() real ext-real Element of REAL
p + ff is V30() real ext-real Element of REAL
sqrt p is V30() real ext-real set
sqrt ff is V30() real ext-real set
(sqrt p) - (sqrt ff) is V30() real ext-real Element of REAL
((sqrt p) - (sqrt ff)) ^2 is V30() real ext-real Element of REAL
((sqrt p) - (sqrt ff)) * ((sqrt p) - (sqrt ff)) is V30() real ext-real set
(sqrt p) ^2 is V30() real ext-real set
(sqrt p) * (sqrt p) is V30() real ext-real set
2 * (sqrt p) is V30() real ext-real Element of REAL
(2 * (sqrt p)) * (sqrt ff) is V30() real ext-real Element of REAL
((sqrt p) ^2) - ((2 * (sqrt p)) * (sqrt ff)) is V30() real ext-real Element of REAL
(sqrt ff) ^2 is V30() real ext-real set
(sqrt ff) * (sqrt ff) is V30() real ext-real set
(((sqrt p) ^2) - ((2 * (sqrt p)) * (sqrt ff))) + ((sqrt ff) ^2) is V30() real ext-real Element of REAL
p - ((2 * (sqrt p)) * (sqrt ff)) is V30() real ext-real Element of REAL
(p - ((2 * (sqrt p)) * (sqrt ff))) + ((sqrt ff) ^2) is V30() real ext-real Element of REAL
(p - ((2 * (sqrt p)) * (sqrt ff))) + ff is V30() real ext-real Element of REAL
(p + ff) - ((2 * (sqrt p)) * (sqrt ff)) is V30() real ext-real Element of REAL
0 + ((2 * (sqrt p)) * (sqrt ff)) is V30() real ext-real Element of REAL
(sqrt p) * (sqrt ff) is V30() real ext-real Element of REAL
2 * ((sqrt p) * (sqrt ff)) is V30() real ext-real Element of REAL
sin | ].0,(PI / 2).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (sin,p) is V30() real ext-real Element of REAL
cos . p is V30() real ext-real Element of REAL
p is V30() real ext-real set
sin . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
- (PI / 2) is V30() real ext-real Element of REAL
(- p) + (PI / 2) is V30() real ext-real Element of REAL
(- (PI / 2)) + (PI / 2) is V30() real ext-real Element of REAL
0 - p is V30() real ext-real Element of REAL
0 + (PI / 2) is V30() real ext-real Element of REAL
(PI / 2) - p is V30() real ext-real Element of REAL
cos . ((PI / 2) - p) is V30() real ext-real Element of REAL
].(PI / 2),PI.[ is open V52() V53() V54() Element of K19(REAL)
sin | ].(PI / 2),PI.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (sin,p) is V30() real ext-real Element of REAL
PI - (PI / 2) is V30() real ext-real Element of REAL
p - (PI / 2) is V30() real ext-real Element of REAL
(PI / 2) - (PI / 2) is V30() real ext-real Element of REAL
sin . (p - (PI / 2)) is V30() real ext-real Element of REAL
0 - (sin . (p - (PI / 2))) is V30() real ext-real Element of REAL
(PI / 2) + (p - (PI / 2)) is V30() real ext-real Element of REAL
cos . ((PI / 2) + (p - (PI / 2))) is V30() real ext-real Element of REAL
- (sin . (p - (PI / 2))) is V30() real ext-real Element of REAL
cos | ].0,(PI / 2).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (cos,p) is V30() real ext-real Element of REAL
sin . p is V30() real ext-real Element of REAL
- (sin . p) is V30() real ext-real Element of REAL
0 - (sin . p) is V30() real ext-real Element of REAL
cos | ].(PI / 2),PI.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (cos,p) is V30() real ext-real Element of REAL
PI - (PI / 2) is V30() real ext-real Element of REAL
p - (PI / 2) is V30() real ext-real Element of REAL
(PI / 2) - (PI / 2) is V30() real ext-real Element of REAL
cos . (p - (PI / 2)) is V30() real ext-real Element of REAL
0 - (cos . (p - (PI / 2))) is V30() real ext-real Element of REAL
(PI / 2) + (p - (PI / 2)) is V30() real ext-real Element of REAL
sin . ((PI / 2) + (p - (PI / 2))) is V30() real ext-real Element of REAL
- (sin . ((PI / 2) + (p - (PI / 2)))) is V30() real ext-real Element of REAL
- (cos . (p - (PI / 2))) is V30() real ext-real Element of REAL
3 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
3 / 2 is V30() real ext-real non negative Element of REAL
(3 / 2) * PI is V30() real ext-real Element of REAL
].PI,((3 / 2) * PI).[ is open V52() V53() V54() Element of K19(REAL)
sin | ].PI,((3 / 2) * PI).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (sin,p) is V30() real ext-real Element of REAL
((3 / 2) * PI) - PI is V30() real ext-real Element of REAL
p - PI is V30() real ext-real Element of REAL
PI - PI is V30() real ext-real Element of REAL
cos . (p - PI) is V30() real ext-real Element of REAL
0 - (cos . (p - PI)) is V30() real ext-real Element of REAL
PI + (p - PI) is V30() real ext-real Element of REAL
cos . (PI + (p - PI)) is V30() real ext-real Element of REAL
- (cos . (p - PI)) is V30() real ext-real Element of REAL
].((3 / 2) * PI),(2 * PI).[ is open V52() V53() V54() Element of K19(REAL)
sin | ].((3 / 2) * PI),(2 * PI).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (sin,p) is V30() real ext-real Element of REAL
(2 * PI) - ((3 / 2) * PI) is V30() real ext-real Element of REAL
p - ((3 / 2) * PI) is V30() real ext-real Element of REAL
(PI / 2) + (p - ((3 / 2) * PI)) is V30() real ext-real Element of REAL
PI + ((PI / 2) + (p - ((3 / 2) * PI))) is V30() real ext-real Element of REAL
cos . (PI + ((PI / 2) + (p - ((3 / 2) * PI)))) is V30() real ext-real Element of REAL
cos . ((PI / 2) + (p - ((3 / 2) * PI))) is V30() real ext-real Element of REAL
- (cos . ((PI / 2) + (p - ((3 / 2) * PI)))) is V30() real ext-real Element of REAL
sin . (p - ((3 / 2) * PI)) is V30() real ext-real Element of REAL
- (sin . (p - ((3 / 2) * PI))) is V30() real ext-real Element of REAL
- (- (sin . (p - ((3 / 2) * PI)))) is V30() real ext-real Element of REAL
((3 / 2) * PI) - ((3 / 2) * PI) is V30() real ext-real Element of REAL
cos | ].PI,((3 / 2) * PI).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (cos,p) is V30() real ext-real Element of REAL
((3 / 2) * PI) - PI is V30() real ext-real Element of REAL
p - PI is V30() real ext-real Element of REAL
PI + (p - PI) is V30() real ext-real Element of REAL
sin . (PI + (p - PI)) is V30() real ext-real Element of REAL
- (sin . (PI + (p - PI))) is V30() real ext-real Element of REAL
sin . (p - PI) is V30() real ext-real Element of REAL
- (sin . (p - PI)) is V30() real ext-real Element of REAL
- (- (sin . (p - PI))) is V30() real ext-real Element of REAL
PI - PI is V30() real ext-real Element of REAL
cos | ].((3 / 2) * PI),(2 * PI).[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
diff (cos,p) is V30() real ext-real Element of REAL
(2 * PI) - ((3 / 2) * PI) is V30() real ext-real Element of REAL
p - ((3 / 2) * PI) is V30() real ext-real Element of REAL
(PI / 2) + (p - ((3 / 2) * PI)) is V30() real ext-real Element of REAL
PI + ((PI / 2) + (p - ((3 / 2) * PI))) is V30() real ext-real Element of REAL
sin . (PI + ((PI / 2) + (p - ((3 / 2) * PI)))) is V30() real ext-real Element of REAL
- (sin . (PI + ((PI / 2) + (p - ((3 / 2) * PI))))) is V30() real ext-real Element of REAL
sin . ((PI / 2) + (p - ((3 / 2) * PI))) is V30() real ext-real Element of REAL
- (sin . ((PI / 2) + (p - ((3 / 2) * PI)))) is V30() real ext-real Element of REAL
- (- (sin . ((PI / 2) + (p - ((3 / 2) * PI))))) is V30() real ext-real Element of REAL
cos . (p - ((3 / 2) * PI)) is V30() real ext-real Element of REAL
((3 / 2) * PI) - ((3 / 2) * PI) is V30() real ext-real Element of REAL
p is V30() real ext-real set
sin . p is V30() real ext-real Element of REAL
ff is ordinal natural V30() real ext-real non negative set
(2 * PI) * ff is V30() real ext-real Element of REAL
((2 * PI) * ff) + p is V30() real ext-real Element of REAL
sin . (((2 * PI) * ff) + p) is V30() real ext-real Element of REAL
p is ordinal natural V30() real ext-real non negative set
(2 * PI) * p is V30() real ext-real Element of REAL
p + 1 is non empty ordinal natural V30() real ext-real positive non negative Element of REAL
(2 * PI) * (p + 1) is V30() real ext-real Element of REAL
f1 is V30() real ext-real set
sin . f1 is V30() real ext-real Element of REAL
((2 * PI) * (p + 1)) + f1 is V30() real ext-real Element of REAL
sin . (((2 * PI) * (p + 1)) + f1) is V30() real ext-real Element of REAL
((2 * PI) * p) + f1 is V30() real ext-real Element of REAL
(((2 * PI) * p) + f1) + (2 * PI) is V30() real ext-real Element of REAL
sin . ((((2 * PI) * p) + f1) + (2 * PI)) is V30() real ext-real Element of REAL
sin . (((2 * PI) * p) + f1) is V30() real ext-real Element of REAL
f1 is V30() real ext-real set
sin . f1 is V30() real ext-real Element of REAL
((2 * PI) * (p + 1)) + f1 is V30() real ext-real Element of REAL
sin . (((2 * PI) * (p + 1)) + f1) is V30() real ext-real Element of REAL
(2 * PI) * 0 is V30() real ext-real Element of REAL
p is V30() real ext-real set
sin . p is V30() real ext-real Element of REAL
((2 * PI) * 0) + p is V30() real ext-real Element of REAL
sin . (((2 * PI) * 0) + p) is V30() real ext-real Element of REAL
p is V30() real ext-real set
cos . p is V30() real ext-real Element of REAL
ff is ordinal natural V30() real ext-real non negative set
(2 * PI) * ff is V30() real ext-real Element of REAL
((2 * PI) * ff) + p is V30() real ext-real Element of REAL
cos . (((2 * PI) * ff) + p) is V30() real ext-real Element of REAL
p is ordinal natural V30() real ext-real non negative set
(2 * PI) * p is V30() real ext-real Element of REAL
p + 1 is non empty ordinal natural V30() real ext-real positive non negative Element of REAL
(2 * PI) * (p + 1) is V30() real ext-real Element of REAL
f1 is V30() real ext-real set
cos . f1 is V30() real ext-real Element of REAL
((2 * PI) * (p + 1)) + f1 is V30() real ext-real Element of REAL
cos . (((2 * PI) * (p + 1)) + f1) is V30() real ext-real Element of REAL
((2 * PI) * p) + f1 is V30() real ext-real Element of REAL
(((2 * PI) * p) + f1) + (2 * PI) is V30() real ext-real Element of REAL
cos . ((((2 * PI) * p) + f1) + (2 * PI)) is V30() real ext-real Element of REAL
cos . (((2 * PI) * p) + f1) is V30() real ext-real Element of REAL
f1 is V30() real ext-real set
cos . f1 is V30() real ext-real Element of REAL
((2 * PI) * (p + 1)) + f1 is V30() real ext-real Element of REAL
cos . (((2 * PI) * (p + 1)) + f1) is V30() real ext-real Element of REAL
(2 * PI) * 0 is V30() real ext-real Element of REAL
p is V30() real ext-real set
cos . p is V30() real ext-real Element of REAL
((2 * PI) * 0) + p is V30() real ext-real Element of REAL
cos . (((2 * PI) * 0) + p) is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
ff is V30() real ext-real set
p . ff is V30() real ext-real Element of REAL
exp_R . ff is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
exp_R . (- ff) is V30() real ext-real Element of REAL
(exp_R . ff) - (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) - (exp_R . (- ff))) / 2 is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
ff is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
p . p is V30() real ext-real Element of REAL
ff . p is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
() is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is set
() . p is V30() real ext-real Element of REAL
p is set
(p) is set
() . p is V30() real ext-real Element of REAL
p is set
(p) is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
ff is V30() real ext-real set
p . ff is V30() real ext-real Element of REAL
exp_R . ff is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
exp_R . (- ff) is V30() real ext-real Element of REAL
(exp_R . ff) + (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) + (exp_R . (- ff))) / 2 is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
ff is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
p . p is V30() real ext-real Element of REAL
ff . p is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
() is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is set
() . p is V30() real ext-real Element of REAL
p is set
(p) is set
() . p is V30() real ext-real Element of REAL
p is set
(p) is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
ff is V30() real ext-real set
p . ff is V30() real ext-real Element of REAL
exp_R . ff is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
exp_R . (- ff) is V30() real ext-real Element of REAL
(exp_R . ff) - (exp_R . (- ff)) is V30() real ext-real Element of REAL
(exp_R . ff) + (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) - (exp_R . (- ff))) / ((exp_R . ff) + (exp_R . (- ff))) is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
ff is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real Element of REAL
p . p is V30() real ext-real Element of REAL
ff . p is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
() is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is set
() . p is V30() real ext-real Element of REAL
p is set
(p) is set
() . p is V30() real ext-real Element of REAL
p is set
(p) is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
p is V30() real ext-real set
exp_R . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
exp_R . (p + ff) is V30() real ext-real Element of REAL
exp_R . ff is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . ff) is V30() real ext-real Element of REAL
exp_R (p + ff) is V30() real ext-real Element of REAL
exp_R p is V30() real ext-real set
exp_R ff is V30() real ext-real set
(exp_R p) * (exp_R ff) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R ff) is V30() real ext-real Element of REAL
exp_R . 0 is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
((() . p) ^2) - ((() . p) ^2) is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real Element of REAL
((() . p) * (() . p)) - ((() . p) * (() . p)) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (() . p) is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . p) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . p) is V30() real ext-real Element of REAL
(((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . (- p)) is V30() real ext-real Element of REAL
((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
2 * 2 is ordinal natural V30() real ext-real non negative Element of REAL
(((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / (2 * 2) is V30() real ext-real Element of REAL
p + p is V30() real ext-real Element of REAL
exp_R . (p + p) is V30() real ext-real Element of REAL
(exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
4 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
p + (- p) is V30() real ext-real Element of REAL
exp_R . (p + (- p)) is V30() real ext-real Element of REAL
(exp_R . (p + p)) - (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
(- p) + (- p) is V30() real ext-real Element of REAL
exp_R . ((- p) + (- p)) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (p + p)) - 1 is V30() real ext-real Element of REAL
((exp_R . (p + p)) - 1) - 1 is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - 1) - 1) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) - 1) - 1) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (() . p) is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / (2 * 2) is V30() real ext-real Element of REAL
(exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (p + p)) + (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (p + p)) + 1 is V30() real ext-real Element of REAL
((exp_R . (p + p)) + 1) + 1 is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + 1) + 1) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + 1) + 1) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (p + p)) + 2 is V30() real ext-real Element of REAL
((exp_R . (p + p)) + 2) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + 2) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (() . ff) is V30() real ext-real Element of REAL
((((exp_R . p) + (exp_R . (- p))) / 2) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
exp_R . ff is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
exp_R . (- ff) is V30() real ext-real Element of REAL
(exp_R . ff) + (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) + (exp_R . (- ff))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2) is V30() real ext-real Element of REAL
((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (() . ff) is V30() real ext-real Element of REAL
((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2)) + ((((exp_R . p) - (exp_R . (- p))) / 2) * (() . ff)) is V30() real ext-real Element of REAL
(exp_R . ff) - (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) - (exp_R . (- ff))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . ff) - (exp_R . (- ff))) / 2) is V30() real ext-real Element of REAL
((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2)) + ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . ff) - (exp_R . (- ff))) / 2)) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . ff) is V30() real ext-real Element of REAL
2 * ((exp_R . p) * (exp_R . ff)) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . (- ff)) is V30() real ext-real Element of REAL
2 * ((exp_R . (- p)) * (exp_R . (- ff))) is V30() real ext-real Element of REAL
(2 * ((exp_R . p) * (exp_R . ff))) + (2 * ((exp_R . (- p)) * (exp_R . (- ff)))) is V30() real ext-real Element of REAL
4 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
((2 * ((exp_R . p) * (exp_R . ff))) + (2 * ((exp_R . (- p)) * (exp_R . (- ff))))) / 4 is V30() real ext-real Element of REAL
exp_R . (p + ff) is V30() real ext-real Element of REAL
2 * (exp_R . (p + ff)) is V30() real ext-real Element of REAL
(2 * (exp_R . (p + ff))) + (2 * ((exp_R . (- p)) * (exp_R . (- ff)))) is V30() real ext-real Element of REAL
((2 * (exp_R . (p + ff))) + (2 * ((exp_R . (- p)) * (exp_R . (- ff))))) / 4 is V30() real ext-real Element of REAL
(- p) + (- ff) is V30() real ext-real Element of REAL
exp_R . ((- p) + (- ff)) is V30() real ext-real Element of REAL
2 * (exp_R . ((- p) + (- ff))) is V30() real ext-real Element of REAL
(2 * (exp_R . (p + ff))) + (2 * (exp_R . ((- p) + (- ff)))) is V30() real ext-real Element of REAL
((2 * (exp_R . (p + ff))) + (2 * (exp_R . ((- p) + (- ff))))) / 4 is V30() real ext-real Element of REAL
- (p + ff) is V30() real ext-real Element of REAL
exp_R . (- (p + ff)) is V30() real ext-real Element of REAL
(exp_R . (p + ff)) + (exp_R . (- (p + ff))) is V30() real ext-real Element of REAL
((exp_R . (p + ff)) + (exp_R . (- (p + ff)))) / 2 is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (() . ff) is V30() real ext-real Element of REAL
((((exp_R . p) - (exp_R . (- p))) / 2) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
exp_R . ff is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
exp_R . (- ff) is V30() real ext-real Element of REAL
(exp_R . ff) + (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) + (exp_R . (- ff))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2) is V30() real ext-real Element of REAL
((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (() . ff) is V30() real ext-real Element of REAL
((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (() . ff)) is V30() real ext-real Element of REAL
(exp_R . ff) - (exp_R . (- ff)) is V30() real ext-real Element of REAL
((exp_R . ff) - (exp_R . (- ff))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . ff) - (exp_R . (- ff))) / 2) is V30() real ext-real Element of REAL
((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . ff) + (exp_R . (- ff))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . ff) - (exp_R . (- ff))) / 2)) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . ff) is V30() real ext-real Element of REAL
2 * ((exp_R . p) * (exp_R . ff)) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . (- ff)) is V30() real ext-real Element of REAL
- ((exp_R . (- p)) * (exp_R . (- ff))) is V30() real ext-real Element of REAL
2 * (- ((exp_R . (- p)) * (exp_R . (- ff)))) is V30() real ext-real Element of REAL
(2 * ((exp_R . p) * (exp_R . ff))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- ff))))) is V30() real ext-real Element of REAL
4 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
((2 * ((exp_R . p) * (exp_R . ff))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- ff)))))) / 4 is V30() real ext-real Element of REAL
exp_R . (p + ff) is V30() real ext-real Element of REAL
2 * (exp_R . (p + ff)) is V30() real ext-real Element of REAL
(2 * (exp_R . (p + ff))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- ff))))) is V30() real ext-real Element of REAL
((2 * (exp_R . (p + ff))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- ff)))))) / 4 is V30() real ext-real Element of REAL
(- p) + (- ff) is V30() real ext-real Element of REAL
exp_R . ((- p) + (- ff)) is V30() real ext-real Element of REAL
- (exp_R . ((- p) + (- ff))) is V30() real ext-real Element of REAL
2 * (- (exp_R . ((- p) + (- ff)))) is V30() real ext-real Element of REAL
(2 * (exp_R . (p + ff))) + (2 * (- (exp_R . ((- p) + (- ff))))) is V30() real ext-real Element of REAL
((2 * (exp_R . (p + ff))) + (2 * (- (exp_R . ((- p) + (- ff)))))) / 4 is V30() real ext-real Element of REAL
- (p + ff) is V30() real ext-real Element of REAL
exp_R . (- (p + ff)) is V30() real ext-real Element of REAL
(exp_R . (p + ff)) - (exp_R . (- (p + ff))) is V30() real ext-real Element of REAL
((exp_R . (p + ff)) - (exp_R . (- (p + ff)))) / 2 is V30() real ext-real Element of REAL
() . 0 is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
- 0 is empty V30() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL
exp_R . (- 0) is V30() real ext-real Element of REAL
(exp_R . 0) + (exp_R . (- 0)) is V30() real ext-real Element of REAL
((exp_R . 0) + (exp_R . (- 0))) / 2 is V30() real ext-real Element of REAL
() . 0 is V30() real ext-real Element of REAL
- 0 is empty V30() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL
exp_R . (- 0) is V30() real ext-real Element of REAL
(exp_R . 0) - (exp_R . (- 0)) is V30() real ext-real Element of REAL
((exp_R . 0) - (exp_R . (- 0))) / 2 is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) / (() . p) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) / (() . p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) / (((exp_R . p) + (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V30() real ext-real set
p * ff is V30() real ext-real Element of REAL
p is V30() real ext-real set
p * ff is V30() real ext-real Element of REAL
p / p is V30() real ext-real Element of REAL
f1 is V30() real ext-real set
p * f1 is V30() real ext-real Element of REAL
(p * ff) + (p * f1) is V30() real ext-real Element of REAL
p * f1 is V30() real ext-real Element of REAL
(p * ff) + (p * f1) is V30() real ext-real Element of REAL
((p * ff) + (p * f1)) / ((p * ff) + (p * f1)) is V30() real ext-real Element of REAL
f1 / ff is V30() real ext-real Element of REAL
(p / p) + (f1 / ff) is V30() real ext-real Element of REAL
(p / p) * (f1 / ff) is V30() real ext-real Element of REAL
1 + ((p / p) * (f1 / ff)) is V30() real ext-real Element of REAL
((p / p) + (f1 / ff)) / (1 + ((p / p) * (f1 / ff))) is V30() real ext-real Element of REAL
((p * ff) + (p * f1)) / (p * ff) is V30() real ext-real Element of REAL
((p * ff) + (p * f1)) / (p * ff) is V30() real ext-real Element of REAL
(((p * ff) + (p * f1)) / (p * ff)) / (((p * ff) + (p * f1)) / (p * ff)) is V30() real ext-real Element of REAL
(p * ff) / (p * ff) is V30() real ext-real Element of REAL
(p * f1) / (p * ff) is V30() real ext-real Element of REAL
((p * ff) / (p * ff)) + ((p * f1) / (p * ff)) is V30() real ext-real Element of REAL
(((p * ff) / (p * ff)) + ((p * f1) / (p * ff))) / (((p * ff) + (p * f1)) / (p * ff)) is V30() real ext-real Element of REAL
(p * ff) / (p * ff) is V30() real ext-real Element of REAL
(p * f1) / (p * ff) is V30() real ext-real Element of REAL
((p * ff) / (p * ff)) + ((p * f1) / (p * ff)) is V30() real ext-real Element of REAL
(((p * ff) / (p * ff)) + ((p * f1) / (p * ff))) / (((p * ff) / (p * ff)) + ((p * f1) / (p * ff))) is V30() real ext-real Element of REAL
f1 * p is V30() real ext-real Element of REAL
ff * p is V30() real ext-real Element of REAL
(f1 * p) / (ff * p) is V30() real ext-real Element of REAL
(p / p) + ((f1 * p) / (ff * p)) is V30() real ext-real Element of REAL
((p / p) + ((f1 * p) / (ff * p))) / (((p * ff) / (p * ff)) + ((p * f1) / (p * ff))) is V30() real ext-real Element of REAL
((p / p) + (f1 / ff)) / (((p * ff) / (p * ff)) + ((p * f1) / (p * ff))) is V30() real ext-real Element of REAL
1 + ((p * f1) / (p * ff)) is V30() real ext-real Element of REAL
((p / p) + (f1 / ff)) / (1 + ((p * f1) / (p * ff))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) + (() . ff) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
1 + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((() . p) + (() . ff)) / (1 + ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
(() . (p + ff)) / (() . (p + ff)) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) / (() . (p + ff)) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) / (((() . p) * (() . ff)) + ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
(() . p) / (() . p) is V30() real ext-real Element of REAL
(() . ff) / (() . ff) is V30() real ext-real Element of REAL
((() . p) / (() . p)) + ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
((() . p) / (() . p)) * ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
1 + (((() . p) / (() . p)) * ((() . ff) / (() . ff))) is V30() real ext-real Element of REAL
(((() . p) / (() . p)) + ((() . ff) / (() . ff))) / (1 + (((() . p) / (() . p)) * ((() . ff) / (() . ff)))) is V30() real ext-real Element of REAL
(() . p) + ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
((() . p) + ((() . ff) / (() . ff))) / (1 + (((() . p) / (() . p)) * ((() . ff) / (() . ff)))) is V30() real ext-real Element of REAL
((() . p) + (() . ff)) / (1 + (((() . p) / (() . p)) * ((() . ff) / (() . ff)))) is V30() real ext-real Element of REAL
(() . p) * ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
1 + ((() . p) * ((() . ff) / (() . ff))) is V30() real ext-real Element of REAL
((() . p) + (() . ff)) / (1 + ((() . p) * ((() . ff) / (() . ff)))) is V30() real ext-real Element of REAL
1 / 2 is V30() real ext-real non negative Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
2 * p is V30() real ext-real Element of REAL
() . (2 * p) is V30() real ext-real Element of REAL
(() . (2 * p)) - 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . (2 * p)) - 1) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
(() . (2 * p)) + 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . (2 * p)) + 1) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (() . p) is V30() real ext-real Element of REAL
(((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . p) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . p) is V30() real ext-real Element of REAL
(((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . (- p)) is V30() real ext-real Element of REAL
((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
4 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
(((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
p + p is V30() real ext-real Element of REAL
exp_R . (p + p) is V30() real ext-real Element of REAL
(exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
(- p) + (- p) is V30() real ext-real Element of REAL
exp_R . ((- p) + (- p)) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
p + (- p) is V30() real ext-real Element of REAL
exp_R . (p + (- p)) is V30() real ext-real Element of REAL
(exp_R . (p + p)) + (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
((exp_R . (p + p)) + (exp_R . (p + (- p)))) + (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + (exp_R . (p + (- p)))) + (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
exp_R . (2 * p) is V30() real ext-real Element of REAL
2 * (exp_R . 0) is V30() real ext-real Element of REAL
(exp_R . (2 * p)) + (2 * (exp_R . 0)) is V30() real ext-real Element of REAL
((exp_R . (2 * p)) + (2 * (exp_R . 0))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
(((exp_R . (2 * p)) + (2 * (exp_R . 0))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
2 * 1 is ordinal natural V30() real ext-real non negative Element of REAL
(exp_R . (2 * p)) + (2 * 1) is V30() real ext-real Element of REAL
- (2 * p) is V30() real ext-real Element of REAL
exp_R . (- (2 * p)) is V30() real ext-real Element of REAL
((exp_R . (2 * p)) + (2 * 1)) + (exp_R . (- (2 * p))) is V30() real ext-real Element of REAL
(((exp_R . (2 * p)) + (2 * 1)) + (exp_R . (- (2 * p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (2 * p)) + (exp_R . (- (2 * p))) is V30() real ext-real Element of REAL
((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2 is V30() real ext-real Element of REAL
(1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2) is V30() real ext-real Element of REAL
1 * 2 is ordinal natural V30() real ext-real non negative Element of REAL
2 * 2 is ordinal natural V30() real ext-real non negative Element of REAL
(1 * 2) / (2 * 2) is V30() real ext-real non negative Element of REAL
((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + ((1 * 2) / (2 * 2)) is V30() real ext-real Element of REAL
(1 / 2) * (() . (2 * p)) is V30() real ext-real Element of REAL
(2 * 1) / 2 is V30() real ext-real non negative Element of REAL
(1 / 2) * ((2 * 1) / 2) is V30() real ext-real non negative Element of REAL
((1 / 2) * (() . (2 * p))) + ((1 / 2) * ((2 * 1) / 2)) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (() . p) is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p)) is V30() real ext-real Element of REAL
((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
(exp_R . (p + p)) - (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
- (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
(exp_R . (p + p)) + (- (exp_R . (p + (- p)))) is V30() real ext-real Element of REAL
((exp_R . (p + p)) + (- (exp_R . (p + (- p))))) - (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
(((exp_R . (p + p)) + (- (exp_R . (p + (- p))))) - (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
((((exp_R . (p + p)) + (- (exp_R . (p + (- p))))) - (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
- (exp_R . 0) is V30() real ext-real Element of REAL
2 * (- (exp_R . 0)) is V30() real ext-real Element of REAL
(exp_R . (2 * p)) + (2 * (- (exp_R . 0))) is V30() real ext-real Element of REAL
((exp_R . (2 * p)) + (2 * (- (exp_R . 0)))) + (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
(((exp_R . (2 * p)) + (2 * (- (exp_R . 0)))) + (exp_R . ((- p) + (- p)))) / 4 is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
2 * (- 1) is V30() real ext-real non positive Element of REAL
(exp_R . (2 * p)) + (2 * (- 1)) is V30() real ext-real Element of REAL
((exp_R . (2 * p)) + (2 * (- 1))) + (exp_R . (- (2 * p))) is V30() real ext-real Element of REAL
(((exp_R . (2 * p)) + (2 * (- 1))) + (exp_R . (- (2 * p)))) / 4 is V30() real ext-real Element of REAL
(- 1) * 2 is V30() real ext-real non positive Element of REAL
((- 1) * 2) / (2 * 2) is V30() real ext-real non positive Element of REAL
((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + (((- 1) * 2) / (2 * 2)) is V30() real ext-real Element of REAL
(2 * (- 1)) / 2 is V30() real ext-real non positive Element of REAL
(1 / 2) * ((2 * (- 1)) / 2) is V30() real ext-real non positive Element of REAL
((1 / 2) * (() . (2 * p))) + ((1 / 2) * ((2 * (- 1)) / 2)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
2 * p is V30() real ext-real Element of REAL
() . (2 * p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
2 * (() . p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(2 * (() . p)) * (() . p) is V30() real ext-real Element of REAL
() . (2 * p) is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
2 * ((() . p) ^2) is V30() real ext-real Element of REAL
(2 * ((() . p) ^2)) - 1 is V30() real ext-real Element of REAL
(() . (2 * p)) + 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . (2 * p)) + 1) is V30() real ext-real Element of REAL
2 * ((1 / 2) * ((() . (2 * p)) + 1)) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
2 * (((exp_R . p) - (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
(2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (() . p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (((exp_R . p) + (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
4 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
2 / 4 is V30() real ext-real non negative Element of REAL
(exp_R . p) ^2 is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . p) is V30() real ext-real set
(exp_R . (- p)) ^2 is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . (- p)) is V30() real ext-real set
((exp_R . p) ^2) - ((exp_R . (- p)) ^2) is V30() real ext-real Element of REAL
(2 / 4) * (((exp_R . p) ^2) - ((exp_R . (- p)) ^2)) is V30() real ext-real Element of REAL
p + p is V30() real ext-real Element of REAL
exp_R . (p + p) is V30() real ext-real Element of REAL
(exp_R . (- p)) * (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . (p + p)) - ((exp_R . (- p)) * (exp_R . (- p))) is V30() real ext-real Element of REAL
(2 / 4) * ((exp_R . (p + p)) - ((exp_R . (- p)) * (exp_R . (- p)))) is V30() real ext-real Element of REAL
exp_R . (2 * p) is V30() real ext-real Element of REAL
(- p) + (- p) is V30() real ext-real Element of REAL
exp_R . ((- p) + (- p)) is V30() real ext-real Element of REAL
(exp_R . (2 * p)) - (exp_R . ((- p) + (- p))) is V30() real ext-real Element of REAL
(2 / 4) * ((exp_R . (2 * p)) - (exp_R . ((- p) + (- p)))) is V30() real ext-real Element of REAL
- (2 * p) is V30() real ext-real Element of REAL
exp_R . (- (2 * p)) is V30() real ext-real Element of REAL
(exp_R . (2 * p)) - (exp_R . (- (2 * p))) is V30() real ext-real Element of REAL
((exp_R . (2 * p)) - (exp_R . (- (2 * p)))) / 2 is V30() real ext-real Element of REAL
(((exp_R . (2 * p)) - (exp_R . (- (2 * p)))) / 2) * 1 is V30() real ext-real Element of REAL
p is V30() real ext-real set
- p is V30() real ext-real Element of REAL
() . (- p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . (- p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
- (() . p) is V30() real ext-real Element of REAL
() . (- p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
- (() . p) is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
- (- p) is V30() real ext-real Element of REAL
exp_R . (- (- p)) is V30() real ext-real Element of REAL
(exp_R . (- p)) + (exp_R . (- (- p))) is V30() real ext-real Element of REAL
((exp_R . (- p)) + (exp_R . (- (- p)))) / 2 is V30() real ext-real Element of REAL
(exp_R . (- p)) - (exp_R . (- (- p))) is V30() real ext-real Element of REAL
((exp_R . (- p)) - (exp_R . (- (- p)))) / 2 is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
- (((exp_R . p) - (exp_R . (- p))) / 2) is V30() real ext-real Element of REAL
(- (() . p)) / (() . (- p)) is V30() real ext-real Element of REAL
(() . p) / (() . p) is V30() real ext-real Element of REAL
- ((() . p) / (() . p)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p - ff is V30() real ext-real Element of REAL
() . (p - ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) - ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
p + (- ff) is V30() real ext-real Element of REAL
() . (p + (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
((() . p) * (() . (- ff))) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
- (() . ff) is V30() real ext-real Element of REAL
(() . p) * (- (() . ff)) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (- (() . ff))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
f1 is V30() real ext-real set
p - f1 is V30() real ext-real Element of REAL
() . (p - f1) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . p) * (() . f1) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . p) * (() . f1) is V30() real ext-real Element of REAL
((() . p) * (() . f1)) - ((() . p) * (() . f1)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p - ff is V30() real ext-real Element of REAL
() . (p - ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) - ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
p + (- ff) is V30() real ext-real Element of REAL
() . (p + (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
((() . p) * (() . (- ff))) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
- (() . ff) is V30() real ext-real Element of REAL
(() . p) * (- (() . ff)) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (- (() . ff))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
f1 is V30() real ext-real set
p - f1 is V30() real ext-real Element of REAL
() . (p - f1) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . p) * (() . f1) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . p) * (() . f1) is V30() real ext-real Element of REAL
((() . p) * (() . f1)) - ((() . p) * (() . f1)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
p - ff is V30() real ext-real Element of REAL
() . (p - ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) - (() . ff) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
1 - ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((() . p) - (() . ff)) / (1 - ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
p + (- ff) is V30() real ext-real Element of REAL
() . (p + (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) + (() . (- ff)) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
1 + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
((() . p) + (() . (- ff))) / (1 + ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
- (() . ff) is V30() real ext-real Element of REAL
(() . p) + (- (() . ff)) is V30() real ext-real Element of REAL
((() . p) + (- (() . ff))) / (1 + ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
(() . p) * (- (() . ff)) is V30() real ext-real Element of REAL
1 + ((() . p) * (- (() . ff))) is V30() real ext-real Element of REAL
((() . p) - (() . ff)) / (1 + ((() . p) * (- (() . ff)))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V30() real ext-real set
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) + (() . ff) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
1 + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((() . p) + (() . ff)) / (1 + ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
f1 is V30() real ext-real set
p - f1 is V30() real ext-real Element of REAL
() . (p - f1) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . p) - (() . f1) is V30() real ext-real Element of REAL
(() . p) * (() . f1) is V30() real ext-real Element of REAL
1 - ((() . p) * (() . f1)) is V30() real ext-real Element of REAL
((() . p) - (() . f1)) / (1 - ((() . p) * (() . f1))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
2 * p is V30() real ext-real Element of REAL
() . (2 * p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
2 * (() . p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(2 * (() . p)) * (() . p) is V30() real ext-real Element of REAL
() . (2 * p) is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
2 * ((() . p) ^2) is V30() real ext-real Element of REAL
(2 * ((() . p) ^2)) - 1 is V30() real ext-real Element of REAL
() . (2 * p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
2 * (() . p) is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
1 + ((() . p) ^2) is V30() real ext-real Element of REAL
(2 * (() . p)) / (1 + ((() . p) ^2)) is V30() real ext-real Element of REAL
p + p is V30() real ext-real Element of REAL
() . (p + p) is V30() real ext-real Element of REAL
(() . p) + (() . p) is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real Element of REAL
1 + ((() . p) * (() . p)) is V30() real ext-real Element of REAL
((() . p) + (() . p)) / (1 + ((() . p) * (() . p))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
ff is V30() real ext-real set
() . ff is V30() real ext-real Element of REAL
(() . ff) ^2 is V30() real ext-real Element of REAL
(() . ff) * (() . ff) is V30() real ext-real set
((() . p) ^2) - ((() . ff) ^2) is V30() real ext-real Element of REAL
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
p - ff is V30() real ext-real Element of REAL
() . (p - ff) is V30() real ext-real Element of REAL
(() . (p + ff)) * (() . (p - ff)) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . ff) ^2 is V30() real ext-real Element of REAL
(() . ff) * (() . ff) is V30() real ext-real set
((() . p) ^2) - ((() . ff) ^2) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
p + (- ff) is V30() real ext-real Element of REAL
() . (p + (- ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) * (() . (p + (- ff))) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
((() . p) * (() . (- ff))) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) * (((() . p) * (() . (- ff))) + ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) * (((() . p) * (() . ff)) + ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
- (() . ff) is V30() real ext-real Element of REAL
(() . p) * (- (() . ff)) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (- (() . ff))) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) * (((() . p) * (() . ff)) + ((() . p) * (- (() . ff)))) is V30() real ext-real Element of REAL
((() . p) ^2) * ((() . ff) ^2) is V30() real ext-real Element of REAL
((() . ff) ^2) * ((() . p) ^2) is V30() real ext-real Element of REAL
(((() . p) ^2) * ((() . ff) ^2)) - (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . p) ^2) - ((() . p) ^2) is V30() real ext-real Element of REAL
- (((() . p) ^2) - ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . ff) ^2) * (- (((() . p) ^2) - ((() . p) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) * ((() . ff) ^2) is V30() real ext-real Element of REAL
- (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
(((() . p) ^2) * ((() . ff) ^2)) + (- (((() . ff) ^2) * ((() . p) ^2))) is V30() real ext-real Element of REAL
(((() . ff) ^2) * (- (((() . p) ^2) - ((() . p) ^2)))) + ((((() . p) ^2) * ((() . ff) ^2)) + (- (((() . ff) ^2) * ((() . p) ^2)))) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
((() . ff) ^2) * (- 1) is V30() real ext-real Element of REAL
((() . ff) ^2) - ((() . ff) ^2) is V30() real ext-real Element of REAL
((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2)) is V30() real ext-real Element of REAL
(((() . ff) ^2) * (- 1)) + (((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) * 1 is V30() real ext-real Element of REAL
(((() . ff) ^2) * (- 1)) + (((() . p) ^2) * 1) is V30() real ext-real Element of REAL
((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2)) is V30() real ext-real Element of REAL
((() . ff) ^2) * ((() . p) ^2) is V30() real ext-real Element of REAL
(((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2))) + (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
((((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2))) + (((() . ff) ^2) * ((() . p) ^2))) - (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . p) ^2) * 1 is V30() real ext-real Element of REAL
((() . p) ^2) * ((() . ff) ^2) is V30() real ext-real Element of REAL
(((() . p) ^2) * 1) + (((() . p) ^2) * ((() . ff) ^2)) is V30() real ext-real Element of REAL
((((() . p) ^2) * 1) + (((() . p) ^2) * ((() . ff) ^2))) - (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . ff) ^2) * (- (((() . p) ^2) - ((() . p) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) + (((() . ff) ^2) * (- (((() . p) ^2) - ((() . p) ^2)))) is V30() real ext-real Element of REAL
((() . ff) ^2) * (- 1) is V30() real ext-real Element of REAL
((() . p) ^2) + (((() . ff) ^2) * (- 1)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
ff is V30() real ext-real set
() . ff is V30() real ext-real Element of REAL
(() . ff) ^2 is V30() real ext-real Element of REAL
(() . ff) * (() . ff) is V30() real ext-real set
((() . p) ^2) + ((() . ff) ^2) is V30() real ext-real Element of REAL
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
p - ff is V30() real ext-real Element of REAL
() . (p - ff) is V30() real ext-real Element of REAL
(() . (p + ff)) * (() . (p - ff)) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . ff) ^2 is V30() real ext-real Element of REAL
(() . ff) * (() . ff) is V30() real ext-real set
((() . p) ^2) + ((() . ff) ^2) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
- ff is V30() real ext-real Element of REAL
p + (- ff) is V30() real ext-real Element of REAL
() . (p + (- ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) * (() . (p + (- ff))) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
() . (- ff) is V30() real ext-real Element of REAL
(() . p) * (() . (- ff)) is V30() real ext-real Element of REAL
((() . p) * (() . (- ff))) + ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) * (((() . p) * (() . (- ff))) + ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
((((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff))))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . (- ff))) is V30() real ext-real Element of REAL
(((((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff))))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff))))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(() . (- ff)) * (() . p) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . (- ff)) * (() . p)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) * ((() . p) * (() . ff))) + (((() . p) * (() . ff)) * ((() . (- ff)) * (() . p))) is V30() real ext-real Element of REAL
((((() . p) * (() . ff)) * ((() . p) * (() . ff))) + (((() . p) * (() . ff)) * ((() . (- ff)) * (() . p)))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff)))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . (- ff)) * (() . p)) is V30() real ext-real Element of REAL
(((((() . p) * (() . ff)) * ((() . p) * (() . ff))) + (((() . p) * (() . ff)) * ((() . (- ff)) * (() . p)))) + (((() . p) * (() . ff)) * ((() . p) * (() . (- ff))))) + (((() . p) * (() . ff)) * ((() . (- ff)) * (() . p))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) ^2 is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . ff)) is V30() real ext-real set
((() . (- ff)) * (() . p)) * ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) ^2) + (((() . (- ff)) * (() . p)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) * ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((((() . p) * (() . ff)) ^2) + (((() . (- ff)) * (() . p)) * ((() . p) * (() . ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
((() . (- ff)) * (() . p)) * ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((((() . p) * (() . ff)) ^2) + (((() . (- ff)) * (() . p)) * ((() . p) * (() . ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . ff)))) + (((() . (- ff)) * (() . p)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
- (() . ff) is V30() real ext-real Element of REAL
(- (() . ff)) * (() . p) is V30() real ext-real Element of REAL
((- (() . ff)) * (() . p)) * ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) ^2) + (((- (() . ff)) * (() . p)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
((((() . p) * (() . ff)) ^2) + (((- (() . ff)) * (() . p)) * ((() . p) * (() . ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
(((((() . p) * (() . ff)) ^2) + (((- (() . ff)) * (() . p)) * ((() . p) * (() . ff)))) + (((() . p) * (() . ff)) * ((() . p) * (() . ff)))) + (((() . (- ff)) * (() . p)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) ^2) + 0 is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) * (() . ff) is V30() real ext-real Element of REAL
((- 1) * (() . ff)) * (() . p) is V30() real ext-real Element of REAL
(((- 1) * (() . ff)) * (() . p)) * ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((((() . p) * (() . ff)) ^2) + 0) + ((((- 1) * (() . ff)) * (() . p)) * ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
((() . p) ^2) * ((() . ff) ^2) is V30() real ext-real Element of REAL
((() . ff) ^2) * ((() . p) ^2) is V30() real ext-real Element of REAL
(((() . p) ^2) * ((() . ff) ^2)) - (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . ff) ^2) - ((() . ff) ^2) is V30() real ext-real Element of REAL
((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2)) is V30() real ext-real Element of REAL
((() . p) ^2) * ((() . ff) ^2) is V30() real ext-real Element of REAL
(((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2))) + (((() . p) ^2) * ((() . ff) ^2)) is V30() real ext-real Element of REAL
- (((() . ff) ^2) * ((() . p) ^2)) is V30() real ext-real Element of REAL
((((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2))) + (((() . p) ^2) * ((() . ff) ^2))) + (- (((() . ff) ^2) * ((() . p) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) * 1 is V30() real ext-real Element of REAL
(((() . p) ^2) * 1) + (((() . p) ^2) * ((() . ff) ^2)) is V30() real ext-real Element of REAL
((((() . p) ^2) * 1) + (((() . p) ^2) * ((() . ff) ^2))) + (- (((() . ff) ^2) * ((() . p) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) - ((() . p) ^2) is V30() real ext-real Element of REAL
((() . ff) ^2) * (((() . p) ^2) - ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . p) ^2) + (((() . ff) ^2) * (((() . p) ^2) - ((() . p) ^2))) is V30() real ext-real Element of REAL
((() . ff) ^2) * 1 is V30() real ext-real Element of REAL
((() . p) ^2) + (((() . ff) ^2) * 1) is V30() real ext-real Element of REAL
((() . ff) ^2) * (((() . p) ^2) - ((() . p) ^2)) is V30() real ext-real Element of REAL
((() . ff) ^2) * ((() . p) ^2) is V30() real ext-real Element of REAL
((() . p) ^2) * ((() . ff) ^2) is V30() real ext-real Element of REAL
- (((() . p) ^2) * ((() . ff) ^2)) is V30() real ext-real Element of REAL
(((() . ff) ^2) * ((() . p) ^2)) + (- (((() . p) ^2) * ((() . ff) ^2))) is V30() real ext-real Element of REAL
(((() . ff) ^2) * (((() . p) ^2) - ((() . p) ^2))) + ((((() . ff) ^2) * ((() . p) ^2)) + (- (((() . p) ^2) * ((() . ff) ^2)))) is V30() real ext-real Element of REAL
((() . ff) ^2) * 1 is V30() real ext-real Element of REAL
(((() . ff) ^2) * ((() . p) ^2)) - (((() . p) ^2) * ((() . ff) ^2)) is V30() real ext-real Element of REAL
(((() . ff) ^2) * 1) + ((((() . ff) ^2) * ((() . p) ^2)) - (((() . p) ^2) * ((() . ff) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2)) is V30() real ext-real Element of REAL
((() . ff) ^2) + (((() . p) ^2) * (((() . ff) ^2) - ((() . ff) ^2))) is V30() real ext-real Element of REAL
((() . p) ^2) * 1 is V30() real ext-real Element of REAL
((() . ff) ^2) + (((() . p) ^2) * 1) is V30() real ext-real Element of REAL
((() . ff) ^2) + ((() . p) ^2) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
p / 2 is V30() real ext-real Element of REAL
ff is V30() real ext-real set
() . ff is V30() real ext-real Element of REAL
(() . p) + (() . ff) is V30() real ext-real Element of REAL
ff / 2 is V30() real ext-real Element of REAL
(p / 2) + (ff / 2) is V30() real ext-real Element of REAL
() . ((p / 2) + (ff / 2)) is V30() real ext-real Element of REAL
2 * (() . ((p / 2) + (ff / 2))) is V30() real ext-real Element of REAL
(p / 2) - (ff / 2) is V30() real ext-real Element of REAL
() . ((p / 2) - (ff / 2)) is V30() real ext-real Element of REAL
(2 * (() . ((p / 2) + (ff / 2)))) * (() . ((p / 2) - (ff / 2))) is V30() real ext-real Element of REAL
(() . p) - (() . ff) is V30() real ext-real Element of REAL
() . ((p / 2) - (ff / 2)) is V30() real ext-real Element of REAL
2 * (() . ((p / 2) - (ff / 2))) is V30() real ext-real Element of REAL
() . ((p / 2) + (ff / 2)) is V30() real ext-real Element of REAL
(2 * (() . ((p / 2) - (ff / 2)))) * (() . ((p / 2) + (ff / 2))) is V30() real ext-real Element of REAL
() . (p / 2) is V30() real ext-real Element of REAL
() . (ff / 2) is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (ff / 2)) is V30() real ext-real Element of REAL
() . (p / 2) is V30() real ext-real Element of REAL
() . (ff / 2) is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (ff / 2)) is V30() real ext-real Element of REAL
((() . (p / 2)) * (() . (ff / 2))) - ((() . (p / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
2 * (((() . (p / 2)) * (() . (ff / 2))) - ((() . (p / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
(2 * (((() . (p / 2)) * (() . (ff / 2))) - ((() . (p / 2)) * (() . (ff / 2))))) * (() . ((p / 2) + (ff / 2))) is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (ff / 2)) is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (ff / 2)) is V30() real ext-real Element of REAL
((() . (p / 2)) * (() . (ff / 2))) + ((() . (p / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
(2 * (((() . (p / 2)) * (() . (ff / 2))) - ((() . (p / 2)) * (() . (ff / 2))))) * (((() . (p / 2)) * (() . (ff / 2))) + ((() . (p / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
(() . (ff / 2)) * (() . (ff / 2)) is V30() real ext-real Element of REAL
(() . (p / 2)) ^2 is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (p / 2)) is V30() real ext-real set
(() . (p / 2)) ^2 is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (p / 2)) is V30() real ext-real set
((() . (p / 2)) ^2) - ((() . (p / 2)) ^2) is V30() real ext-real Element of REAL
- (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2)) is V30() real ext-real Element of REAL
((() . (ff / 2)) * (() . (ff / 2))) * (- (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2))) is V30() real ext-real Element of REAL
(() . (ff / 2)) ^2 is V30() real ext-real Element of REAL
(() . (ff / 2)) * (() . (ff / 2)) is V30() real ext-real set
(() . (p / 2)) * ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
(() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
(((() . (ff / 2)) * (() . (ff / 2))) * (- (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2)))) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
(() . (ff / 2)) ^2 is V30() real ext-real Element of REAL
(() . (ff / 2)) * (() . (ff / 2)) is V30() real ext-real set
(() . (p / 2)) * ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
(() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
((((() . (ff / 2)) * (() . (ff / 2))) * (- (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2)))) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
2 * (((((() . (ff / 2)) * (() . (ff / 2))) * (- (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2)))) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
((() . (ff / 2)) * (() . (ff / 2))) * (- 1) is V30() real ext-real Element of REAL
(((() . (ff / 2)) * (() . (ff / 2))) * (- 1)) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
((((() . (ff / 2)) * (() . (ff / 2))) * (- 1)) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
2 * (((((() . (ff / 2)) * (() . (ff / 2))) * (- 1)) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (p / 2)) is V30() real ext-real Element of REAL
((() . (ff / 2)) ^2) - ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
((() . (p / 2)) * (() . (p / 2))) * (((() . (ff / 2)) ^2) - ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
(- 1) * ((() . (ff / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
(((() . (p / 2)) * (() . (p / 2))) * (((() . (ff / 2)) ^2) - ((() . (ff / 2)) ^2))) + ((- 1) * ((() . (ff / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
2 * ((((() . (p / 2)) * (() . (p / 2))) * (((() . (ff / 2)) ^2) - ((() . (ff / 2)) ^2))) + ((- 1) * ((() . (ff / 2)) * (() . (ff / 2))))) is V30() real ext-real Element of REAL
((() . (p / 2)) * (() . (p / 2))) * 1 is V30() real ext-real Element of REAL
(((() . (p / 2)) * (() . (p / 2))) * 1) + ((- 1) * ((() . (ff / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
2 * ((((() . (p / 2)) * (() . (p / 2))) * 1) + ((- 1) * ((() . (ff / 2)) * (() . (ff / 2))))) is V30() real ext-real Element of REAL
2 * (() . (p / 2)) is V30() real ext-real Element of REAL
(2 * (() . (p / 2))) * (() . (p / 2)) is V30() real ext-real Element of REAL
(() . (ff / 2)) * (() . (ff / 2)) is V30() real ext-real Element of REAL
2 * ((() . (ff / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
((2 * (() . (p / 2))) * (() . (p / 2))) - (2 * ((() . (ff / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
2 * (p / 2) is V30() real ext-real Element of REAL
() . (2 * (p / 2)) is V30() real ext-real Element of REAL
2 * (() . (ff / 2)) is V30() real ext-real Element of REAL
(2 * (() . (ff / 2))) * (() . (ff / 2)) is V30() real ext-real Element of REAL
(() . (2 * (p / 2))) - ((2 * (() . (ff / 2))) * (() . (ff / 2))) is V30() real ext-real Element of REAL
2 * (ff / 2) is V30() real ext-real Element of REAL
() . (2 * (ff / 2)) is V30() real ext-real Element of REAL
(() . p) - (() . (2 * (ff / 2))) is V30() real ext-real Element of REAL
((() . (p / 2)) * (() . (ff / 2))) + ((() . (p / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
2 * (((() . (p / 2)) * (() . (ff / 2))) + ((() . (p / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
(2 * (((() . (p / 2)) * (() . (ff / 2))) + ((() . (p / 2)) * (() . (ff / 2))))) * (() . ((p / 2) - (ff / 2))) is V30() real ext-real Element of REAL
((() . (p / 2)) * (() . (ff / 2))) - ((() . (p / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
(2 * (((() . (p / 2)) * (() . (ff / 2))) + ((() . (p / 2)) * (() . (ff / 2))))) * (((() . (p / 2)) * (() . (ff / 2))) - ((() . (p / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
((() . (ff / 2)) * (() . (ff / 2))) * (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2)) is V30() real ext-real Element of REAL
(((() . (ff / 2)) * (() . (ff / 2))) * (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2))) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
((((() . (ff / 2)) * (() . (ff / 2))) * (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2))) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
2 * (((((() . (ff / 2)) * (() . (ff / 2))) * (((() . (p / 2)) ^2) - ((() . (p / 2)) ^2))) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) is V30() real ext-real Element of REAL
((() . (ff / 2)) * (() . (ff / 2))) * 1 is V30() real ext-real Element of REAL
(((() . (ff / 2)) * (() . (ff / 2))) * 1) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
((((() . (ff / 2)) * (() . (ff / 2))) * 1) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2))) is V30() real ext-real Element of REAL
2 * (((((() . (ff / 2)) * (() . (ff / 2))) * 1) + ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) - ((() . (p / 2)) * ((() . (p / 2)) * ((() . (ff / 2)) ^2)))) is V30() real ext-real Element of REAL
(((() . (p / 2)) * (() . (p / 2))) * (((() . (ff / 2)) ^2) - ((() . (ff / 2)) ^2))) + ((() . (ff / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
2 * ((((() . (p / 2)) * (() . (p / 2))) * (((() . (ff / 2)) ^2) - ((() . (ff / 2)) ^2))) + ((() . (ff / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
(((() . (p / 2)) * (() . (p / 2))) * 1) + ((() . (ff / 2)) * (() . (ff / 2))) is V30() real ext-real Element of REAL
2 * ((((() . (p / 2)) * (() . (p / 2))) * 1) + ((() . (ff / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
((2 * (() . (p / 2))) * (() . (p / 2))) + (2 * ((() . (ff / 2)) * (() . (ff / 2)))) is V30() real ext-real Element of REAL
(() . (2 * (p / 2))) + ((2 * (() . (ff / 2))) * (() . (ff / 2))) is V30() real ext-real Element of REAL
(() . p) + (() . (2 * (ff / 2))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
p / 2 is V30() real ext-real Element of REAL
ff is V30() real ext-real set
() . ff is V30() real ext-real Element of REAL
(() . p) + (() . ff) is V30() real ext-real Element of REAL
ff / 2 is V30() real ext-real Element of REAL
(p / 2) + (ff / 2) is V30() real ext-real Element of REAL
() . ((p / 2) + (ff / 2)) is V30() real ext-real Element of REAL
2 * (() . ((p / 2) + (ff / 2))) is V30() real ext-real Element of REAL
(p / 2) - (ff / 2) is V30() real ext-real Element of REAL
() . ((p / 2) - (ff / 2)) is V30() real ext-real Element of REAL
(2 * (() . ((p / 2) + (ff / 2)))) * (() . ((p / 2) - (ff / 2))) is V30() real ext-real Element of REAL
(() . p) - (() . ff) is V30() real ext-real Element of REAL
() . ((p / 2) - (ff / 2)) is V30() real ext-real Element of REAL
2 * (() . ((p / 2) - (ff / 2))) is V30() real ext-real Element of REAL
() . ((p / 2) + (ff / 2)) is V30() real ext-real Element of REAL
(2 * (() . ((p / 2) - (ff / 2)))) * (() . ((p / 2) + (ff / 2))) is V30() real ext-real Element of REAL
(() . ((p / 2) - (ff / 2))) * (() . ((p / 2) + (ff / 2))) is V30() real ext-real Element of REAL
2 * ((() . ((p / 2) - (ff / 2))) * (() . ((p / 2) + (ff / 2)))) is V30() real ext-real Element of REAL
() . (p / 2) is V30() real ext-real Element of REAL
(() . (p / 2)) ^2 is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (p / 2)) is V30() real ext-real set
() . (ff / 2) is V30() real ext-real Element of REAL
(() . (ff / 2)) ^2 is V30() real ext-real Element of REAL
(() . (ff / 2)) * (() . (ff / 2)) is V30() real ext-real set
((() . (p / 2)) ^2) - ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
2 * (((() . (p / 2)) ^2) - ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
2 * (p / 2) is V30() real ext-real Element of REAL
() . (2 * (p / 2)) is V30() real ext-real Element of REAL
(() . (2 * (p / 2))) + 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . (2 * (p / 2))) + 1) is V30() real ext-real Element of REAL
((1 / 2) * ((() . (2 * (p / 2))) + 1)) - ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
2 * (((1 / 2) * ((() . (2 * (p / 2))) + 1)) - ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
(() . p) + 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . p) + 1) is V30() real ext-real Element of REAL
2 * (ff / 2) is V30() real ext-real Element of REAL
() . (2 * (ff / 2)) is V30() real ext-real Element of REAL
(() . (2 * (ff / 2))) + 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . (2 * (ff / 2))) + 1) is V30() real ext-real Element of REAL
((1 / 2) * ((() . p) + 1)) - ((1 / 2) * ((() . (2 * (ff / 2))) + 1)) is V30() real ext-real Element of REAL
2 * (((1 / 2) * ((() . p) + 1)) - ((1 / 2) * ((() . (2 * (ff / 2))) + 1))) is V30() real ext-real Element of REAL
(() . ((p / 2) + (ff / 2))) * (() . ((p / 2) - (ff / 2))) is V30() real ext-real Element of REAL
2 * ((() . ((p / 2) + (ff / 2))) * (() . ((p / 2) - (ff / 2)))) is V30() real ext-real Element of REAL
() . (p / 2) is V30() real ext-real Element of REAL
(() . (p / 2)) ^2 is V30() real ext-real Element of REAL
(() . (p / 2)) * (() . (p / 2)) is V30() real ext-real set
((() . (p / 2)) ^2) + ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
2 * (((() . (p / 2)) ^2) + ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
(() . (2 * (p / 2))) - 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . (2 * (p / 2))) - 1) is V30() real ext-real Element of REAL
((1 / 2) * ((() . (2 * (p / 2))) - 1)) + ((() . (ff / 2)) ^2) is V30() real ext-real Element of REAL
2 * (((1 / 2) * ((() . (2 * (p / 2))) - 1)) + ((() . (ff / 2)) ^2)) is V30() real ext-real Element of REAL
(() . p) - 1 is V30() real ext-real Element of REAL
(1 / 2) * ((() . p) - 1) is V30() real ext-real Element of REAL
((1 / 2) * ((() . p) - 1)) + ((1 / 2) * ((() . (2 * (ff / 2))) + 1)) is V30() real ext-real Element of REAL
2 * (((1 / 2) * ((() . p) - 1)) + ((1 / 2) * ((() . (2 * (ff / 2))) + 1))) is V30() real ext-real Element of REAL
(() . ff) + (() . p) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
ff is V30() real ext-real set
() . ff is V30() real ext-real Element of REAL
(() . p) + (() . ff) is V30() real ext-real Element of REAL
p + ff is V30() real ext-real Element of REAL
() . (p + ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
(() . (p + ff)) / ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(() . p) - (() . ff) is V30() real ext-real Element of REAL
p - ff is V30() real ext-real Element of REAL
() . (p - ff) is V30() real ext-real Element of REAL
(() . (p - ff)) / ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . p) * (() . ff) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) - ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) - ((() . p) * (() . ff))) / ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) / ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) / ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) / ((() . p) * (() . ff))) - (((() . p) * (() . ff)) / ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
(() . p) / (() . p) is V30() real ext-real Element of REAL
((() . p) / (() . p)) - (((() . p) * (() . ff)) / ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
(() . ff) / (() . ff) is V30() real ext-real Element of REAL
((() . p) / (() . p)) - ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
(() . p) - ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
((() . p) * (() . ff)) + ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) + ((() . p) * (() . ff))) / ((() . p) * (() . ff)) is V30() real ext-real Element of REAL
(((() . p) * (() . ff)) / ((() . p) * (() . ff))) + (((() . p) * (() . ff)) / ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
((() . p) / (() . p)) + (((() . p) * (() . ff)) / ((() . p) * (() . ff))) is V30() real ext-real Element of REAL
((() . p) / (() . p)) + ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
(() . p) + ((() . ff) / (() . ff)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) + (() . p) is V30() real ext-real Element of REAL
ff is ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
((() . p) + (() . p)) |^ ff is V30() real ext-real Element of REAL
ff * p is V30() real ext-real Element of REAL
() . (ff * p) is V30() real ext-real Element of REAL
() . (ff * p) is V30() real ext-real Element of REAL
(() . (ff * p)) + (() . (ff * p)) is V30() real ext-real Element of REAL
p is ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
p + 1 is non empty ordinal natural V30() real ext-real positive non negative Element of REAL
f1 is V30() real ext-real set
() . f1 is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . f1) + (() . f1) is V30() real ext-real Element of REAL
((() . f1) + (() . f1)) |^ (p + 1) is V30() real ext-real Element of REAL
(p + 1) * f1 is V30() real ext-real Element of REAL
() . ((p + 1) * f1) is V30() real ext-real Element of REAL
() . ((p + 1) * f1) is V30() real ext-real Element of REAL
(() . ((p + 1) * f1)) + (() . ((p + 1) * f1)) is V30() real ext-real Element of REAL
p * f1 is V30() real ext-real Element of REAL
() . (p * f1) is V30() real ext-real Element of REAL
(() . (p * f1)) * (() . f1) is V30() real ext-real Element of REAL
() . (p * f1) is V30() real ext-real Element of REAL
(() . (p * f1)) * (() . f1) is V30() real ext-real Element of REAL
((() . (p * f1)) * (() . f1)) + ((() . (p * f1)) * (() . f1)) is V30() real ext-real Element of REAL
exp_R . (p * f1) is V30() real ext-real Element of REAL
- (p * f1) is V30() real ext-real Element of REAL
exp_R . (- (p * f1)) is V30() real ext-real Element of REAL
(exp_R . (p * f1)) + (exp_R . (- (p * f1))) is V30() real ext-real Element of REAL
((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2 is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (() . f1) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (() . f1)) + ((() . (p * f1)) * (() . f1)) is V30() real ext-real Element of REAL
exp_R . f1 is V30() real ext-real Element of REAL
- f1 is V30() real ext-real Element of REAL
exp_R . (- f1) is V30() real ext-real Element of REAL
(exp_R . f1) + (exp_R . (- f1)) is V30() real ext-real Element of REAL
((exp_R . f1) + (exp_R . (- f1))) / 2 is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) + (exp_R . (- f1))) / 2) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) + (exp_R . (- f1))) / 2)) + ((() . (p * f1)) * (() . f1)) is V30() real ext-real Element of REAL
(exp_R . (p * f1)) - (exp_R . (- (p * f1))) is V30() real ext-real Element of REAL
((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2 is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2) * (() . f1) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) + (exp_R . (- f1))) / 2)) + ((((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2) * (() . f1)) is V30() real ext-real Element of REAL
(exp_R . (p * f1)) / 2 is V30() real ext-real Element of REAL
(exp_R . (- (p * f1))) / 2 is V30() real ext-real Element of REAL
((exp_R . (p * f1)) / 2) + ((exp_R . (- (p * f1))) / 2) is V30() real ext-real Element of REAL
(exp_R . f1) / 2 is V30() real ext-real Element of REAL
(exp_R . (- f1)) / 2 is V30() real ext-real Element of REAL
((exp_R . f1) / 2) + ((exp_R . (- f1)) / 2) is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) / 2) + ((exp_R . (- (p * f1))) / 2)) * (((exp_R . f1) / 2) + ((exp_R . (- f1)) / 2)) is V30() real ext-real Element of REAL
((exp_R . (p * f1)) / 2) - ((exp_R . (- (p * f1))) / 2) is V30() real ext-real Element of REAL
(exp_R . f1) - (exp_R . (- f1)) is V30() real ext-real Element of REAL
((exp_R . f1) - (exp_R . (- f1))) / 2 is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) / 2) - ((exp_R . (- (p * f1))) / 2)) * (((exp_R . f1) - (exp_R . (- f1))) / 2) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) / 2) + ((exp_R . (- (p * f1))) / 2)) * (((exp_R . f1) / 2) + ((exp_R . (- f1)) / 2))) + ((((exp_R . (p * f1)) / 2) - ((exp_R . (- (p * f1))) / 2)) * (((exp_R . f1) - (exp_R . (- f1))) / 2)) is V30() real ext-real Element of REAL
(exp_R . (p * f1)) * (exp_R . f1) is V30() real ext-real Element of REAL
2 * 2 is ordinal natural V30() real ext-real non negative Element of REAL
((exp_R . (p * f1)) * (exp_R . f1)) / (2 * 2) is V30() real ext-real Element of REAL
2 * (((exp_R . (p * f1)) * (exp_R . f1)) / (2 * 2)) is V30() real ext-real Element of REAL
((exp_R . (- (p * f1))) / 2) * ((exp_R . (- f1)) / 2) is V30() real ext-real Element of REAL
2 * (((exp_R . (- (p * f1))) / 2) * ((exp_R . (- f1)) / 2)) is V30() real ext-real Element of REAL
(2 * (((exp_R . (p * f1)) * (exp_R . f1)) / (2 * 2))) + (2 * (((exp_R . (- (p * f1))) / 2) * ((exp_R . (- f1)) / 2))) is V30() real ext-real Element of REAL
f1 * p is V30() real ext-real Element of REAL
f1 * 1 is V30() real ext-real Element of REAL
(f1 * p) + (f1 * 1) is V30() real ext-real Element of REAL
exp_R . ((f1 * p) + (f1 * 1)) is V30() real ext-real Element of REAL
(exp_R . ((f1 * p) + (f1 * 1))) / (2 * 2) is V30() real ext-real Element of REAL
2 * ((exp_R . ((f1 * p) + (f1 * 1))) / (2 * 2)) is V30() real ext-real Element of REAL
(exp_R . (- (p * f1))) * (exp_R . (- f1)) is V30() real ext-real Element of REAL
((exp_R . (- (p * f1))) * (exp_R . (- f1))) / (2 * 2) is V30() real ext-real Element of REAL
2 * (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / (2 * 2)) is V30() real ext-real Element of REAL
(2 * ((exp_R . ((f1 * p) + (f1 * 1))) / (2 * 2))) + (2 * (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / (2 * 2))) is V30() real ext-real Element of REAL
f1 * (p + 1) is V30() real ext-real Element of REAL
exp_R . (f1 * (p + 1)) is V30() real ext-real Element of REAL
(exp_R . (f1 * (p + 1))) / (2 * 2) is V30() real ext-real Element of REAL
2 * ((exp_R . (f1 * (p + 1))) / (2 * 2)) is V30() real ext-real Element of REAL
(- (p * f1)) + (- f1) is V30() real ext-real Element of REAL
exp_R . ((- (p * f1)) + (- f1)) is V30() real ext-real Element of REAL
(exp_R . ((- (p * f1)) + (- f1))) / (2 * 2) is V30() real ext-real Element of REAL
2 * ((exp_R . ((- (p * f1)) + (- f1))) / (2 * 2)) is V30() real ext-real Element of REAL
(2 * ((exp_R . (f1 * (p + 1))) / (2 * 2))) + (2 * ((exp_R . ((- (p * f1)) + (- f1))) / (2 * 2))) is V30() real ext-real Element of REAL
- (f1 * (p + 1)) is V30() real ext-real Element of REAL
exp_R . (- (f1 * (p + 1))) is V30() real ext-real Element of REAL
(exp_R . (f1 * (p + 1))) + (exp_R . (- (f1 * (p + 1)))) is V30() real ext-real Element of REAL
((exp_R . (f1 * (p + 1))) + (exp_R . (- (f1 * (p + 1))))) / 2 is V30() real ext-real Element of REAL
() . (f1 * (p + 1)) is V30() real ext-real Element of REAL
(() . (p * f1)) * (() . f1) is V30() real ext-real Element of REAL
(() . (p * f1)) * (() . f1) is V30() real ext-real Element of REAL
((() . (p * f1)) * (() . f1)) + ((() . (p * f1)) * (() . f1)) is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (() . f1) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (() . f1)) + ((() . (p * f1)) * (() . f1)) is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) - (exp_R . (- f1))) / 2) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) - (exp_R . (- f1))) / 2)) + ((() . (p * f1)) * (() . f1)) is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2) * (() . f1) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) + (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) - (exp_R . (- f1))) / 2)) + ((((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2) * (() . f1)) is V30() real ext-real Element of REAL
((exp_R . (p * f1)) / 2) * ((exp_R . f1) / 2) is V30() real ext-real Element of REAL
((exp_R . (p * f1)) / 2) * ((exp_R . (- f1)) / 2) is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) / 2) * ((exp_R . f1) / 2)) - (((exp_R . (p * f1)) / 2) * ((exp_R . (- f1)) / 2)) is V30() real ext-real Element of REAL
((exp_R . (- (p * f1))) / 2) * ((exp_R . f1) / 2) is V30() real ext-real Element of REAL
((((exp_R . (p * f1)) / 2) * ((exp_R . f1) / 2)) - (((exp_R . (p * f1)) / 2) * ((exp_R . (- f1)) / 2))) + (((exp_R . (- (p * f1))) / 2) * ((exp_R . f1) / 2)) is V30() real ext-real Element of REAL
(((((exp_R . (p * f1)) / 2) * ((exp_R . f1) / 2)) - (((exp_R . (p * f1)) / 2) * ((exp_R . (- f1)) / 2))) + (((exp_R . (- (p * f1))) / 2) * ((exp_R . f1) / 2))) - (((exp_R . (- (p * f1))) / 2) * ((exp_R . (- f1)) / 2)) is V30() real ext-real Element of REAL
(((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) + (exp_R . (- f1))) / 2) is V30() real ext-real Element of REAL
((((((exp_R . (p * f1)) / 2) * ((exp_R . f1) / 2)) - (((exp_R . (p * f1)) / 2) * ((exp_R . (- f1)) / 2))) + (((exp_R . (- (p * f1))) / 2) * ((exp_R . f1) / 2))) - (((exp_R . (- (p * f1))) / 2) * ((exp_R . (- f1)) / 2))) + ((((exp_R . (p * f1)) - (exp_R . (- (p * f1)))) / 2) * (((exp_R . f1) + (exp_R . (- f1))) / 2)) is V30() real ext-real Element of REAL
4 is non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
((exp_R . (p * f1)) * (exp_R . f1)) / 4 is V30() real ext-real Element of REAL
2 * (((exp_R . (p * f1)) * (exp_R . f1)) / 4) is V30() real ext-real Element of REAL
- (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / (2 * 2)) is V30() real ext-real Element of REAL
2 * (- (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / (2 * 2))) is V30() real ext-real Element of REAL
(2 * (((exp_R . (p * f1)) * (exp_R . f1)) / 4)) + (2 * (- (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / (2 * 2)))) is V30() real ext-real Element of REAL
(p * f1) + f1 is V30() real ext-real Element of REAL
exp_R . ((p * f1) + f1) is V30() real ext-real Element of REAL
(exp_R . ((p * f1) + f1)) / 4 is V30() real ext-real Element of REAL
2 * ((exp_R . ((p * f1) + f1)) / 4) is V30() real ext-real Element of REAL
((exp_R . (- (p * f1))) * (exp_R . (- f1))) / 4 is V30() real ext-real Element of REAL
- (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / 4) is V30() real ext-real Element of REAL
2 * (- (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / 4)) is V30() real ext-real Element of REAL
(2 * ((exp_R . ((p * f1) + f1)) / 4)) + (2 * (- (((exp_R . (- (p * f1))) * (exp_R . (- f1))) / 4))) is V30() real ext-real Element of REAL
(exp_R . ((- (p * f1)) + (- f1))) / 4 is V30() real ext-real Element of REAL
- ((exp_R . ((- (p * f1)) + (- f1))) / 4) is V30() real ext-real Element of REAL
2 * (- ((exp_R . ((- (p * f1)) + (- f1))) / 4)) is V30() real ext-real Element of REAL
(2 * ((exp_R . ((p * f1) + f1)) / 4)) + (2 * (- ((exp_R . ((- (p * f1)) + (- f1))) / 4))) is V30() real ext-real Element of REAL
(exp_R . (f1 * (p + 1))) - (exp_R . (- (f1 * (p + 1)))) is V30() real ext-real Element of REAL
((exp_R . (f1 * (p + 1))) - (exp_R . (- (f1 * (p + 1))))) / 2 is V30() real ext-real Element of REAL
() . (f1 * (p + 1)) is V30() real ext-real Element of REAL
((() . f1) + (() . f1)) |^ p is V30() real ext-real Element of REAL
(((() . f1) + (() . f1)) |^ p) * ((() . f1) + (() . f1)) is V30() real ext-real Element of REAL
(() . (p * f1)) + (() . (p * f1)) is V30() real ext-real Element of REAL
((() . (p * f1)) + (() . (p * f1))) * ((() . f1) + (() . f1)) is V30() real ext-real Element of REAL
(() . ((p + 1) * f1)) + (() . ((p + 1) * f1)) is V30() real ext-real Element of REAL
f1 is V30() real ext-real set
() . f1 is V30() real ext-real Element of REAL
() . f1 is V30() real ext-real Element of REAL
(() . f1) + (() . f1) is V30() real ext-real Element of REAL
((() . f1) + (() . f1)) |^ (p + 1) is V30() real ext-real Element of REAL
(p + 1) * f1 is V30() real ext-real Element of REAL
() . ((p + 1) * f1) is V30() real ext-real Element of REAL
() . ((p + 1) * f1) is V30() real ext-real Element of REAL
(() . ((p + 1) * f1)) + (() . ((p + 1) * f1)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) + (() . p) is V30() real ext-real Element of REAL
((() . p) + (() . p)) |^ 0 is V30() real ext-real Element of REAL
0 * p is V30() real ext-real Element of REAL
() . (0 * p) is V30() real ext-real Element of REAL
() . (0 * p) is V30() real ext-real Element of REAL
(() . (0 * p)) + (() . (0 * p)) is V30() real ext-real Element of REAL
dom () is V52() V53() V54() Element of K19(REAL)
dom () is V52() V53() V54() Element of K19(REAL)
dom () is V52() V53() V54() Element of K19(REAL)
- 1 is V30() real ext-real non positive Element of REAL
p is V30() real ext-real set
compreal . p is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
dom compreal is V52() V53() V54() Element of K19(REAL)
REAL --> 0 is V1() V4( REAL ) V5( REAL ) V5( RAT ) V5( INT ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(REAL,REAL))
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real set
diff (ff,p) is V30() real ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom p is V52() V53() V54() Element of K19(REAL)
p is V1() non-zero V4( NAT ) V5( REAL ) V6() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
p " is V1() V4( NAT ) V5( REAL ) V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
p /* p is V1() V4( NAT ) V5( REAL ) V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(p ") (#) (p /* p) is V1() V4( NAT ) V5( REAL ) V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((p ") (#) (p /* p)) is V30() real ext-real Element of REAL
p is ordinal natural V30() real ext-real non negative set
((p ") (#) (p /* p)) . p is V30() real ext-real Element of REAL
rng p is V52() V53() V54() Element of K19(REAL)
(p ") . p is V30() real ext-real Element of REAL
(p /* p) . p is V30() real ext-real Element of REAL
((p ") . p) * ((p /* p) . p) is V30() real ext-real Element of REAL
p . p is V30() real ext-real Element of REAL
(p . p) " is V30() real ext-real Element of REAL
((p . p) ") * ((p /* p) . p) is V30() real ext-real Element of REAL
p . (p . p) is V30() real ext-real Element of REAL
((p . p) ") * (p . (p . p)) is V30() real ext-real Element of REAL
((p . p) ") * 0 is V30() real ext-real Element of REAL
p is ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() Element of NAT
((p ") (#) (p /* p)) . p is V30() real ext-real Element of REAL
compreal . p is V30() real ext-real Element of REAL
p - 1 is V30() real ext-real Element of REAL
p + 1 is V30() real ext-real Element of REAL
].(p - 1),(p + 1).[ is open V52() V53() V54() Element of K19(REAL)
p is V30() real ext-real set
compreal . p is V30() real ext-real Element of REAL
(compreal . p) - (compreal . p) is V30() real ext-real Element of REAL
p - p is V30() real ext-real Element of REAL
f1 . (p - p) is V30() real ext-real Element of REAL
p . (p - p) is V30() real ext-real Element of REAL
(f1 . (p - p)) + (p . (p - p)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
p . p is V30() real ext-real Element of REAL
p is V30() real ext-real set
f1 . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
((- 1) * p) - (compreal . p) is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
((- 1) * p) - ((- 1) * p) is V30() real ext-real Element of REAL
(((- 1) * p) - ((- 1) * p)) + 0 is V30() real ext-real Element of REAL
- (p - p) is V30() real ext-real Element of REAL
(- (p - p)) + (p . (p - p)) is V30() real ext-real Element of REAL
p is V30() real ext-real Element of REAL
compreal . p is V30() real ext-real Element of REAL
(compreal . p) - (compreal . p) is V30() real ext-real Element of REAL
p - p is V30() real ext-real Element of REAL
f1 . (p - p) is V30() real ext-real Element of REAL
p . (p - p) is V30() real ext-real Element of REAL
(f1 . (p - p)) + (p . (p - p)) is V30() real ext-real Element of REAL
p is V30() real ext-real Element of REAL
f1 . p is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
p is open V52() V53() V54() Neighbourhood of p
f1 . 1 is V30() real ext-real Element of REAL
p is open V52() V53() V54() Neighbourhood of p
p is open V52() V53() V54() Neighbourhood of p
p is V30() real ext-real set
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
diff ((exp_R * ff),p) is V30() real ext-real Element of REAL
ff . p is V30() real ext-real Element of REAL
exp_R . (ff . p) is V30() real ext-real Element of REAL
(- 1) * (exp_R . (ff . p)) is V30() real ext-real Element of REAL
diff (exp_R,(ff . p)) is V30() real ext-real Element of REAL
diff (ff,p) is V30() real ext-real Element of REAL
(diff (exp_R,(ff . p))) * (diff (ff,p)) is V30() real ext-real Element of REAL
(diff (exp_R,(ff . p))) * (- 1) is V30() real ext-real Element of REAL
(exp_R . (ff . p)) * (- 1) is V30() real ext-real Element of REAL
p is V30() real ext-real set
(- 1) * p is V30() real ext-real Element of REAL
exp_R . ((- 1) * p) is V30() real ext-real Element of REAL
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(exp_R * ff) . p is V30() real ext-real Element of REAL
ff . p is V30() real ext-real Element of REAL
exp_R . (ff . p) is V30() real ext-real Element of REAL
p is V30() real ext-real set
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R - (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R + (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
diff ((exp_R - (exp_R * ff)),p) is V30() real ext-real Element of REAL
diff ((exp_R + (exp_R * ff)),p) is V30() real ext-real Element of REAL
diff (exp_R,p) is V30() real ext-real Element of REAL
diff ((exp_R * ff),p) is V30() real ext-real Element of REAL
(diff (exp_R,p)) + (diff ((exp_R * ff),p)) is V30() real ext-real Element of REAL
(exp_R . p) + (diff ((exp_R * ff),p)) is V30() real ext-real Element of REAL
ff . p is V30() real ext-real Element of REAL
exp_R . (ff . p) is V30() real ext-real Element of REAL
(- 1) * (exp_R . (ff . p)) is V30() real ext-real Element of REAL
(exp_R . p) + ((- 1) * (exp_R . (ff . p))) is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
exp_R . ((- 1) * p) is V30() real ext-real Element of REAL
(- 1) * (exp_R . ((- 1) * p)) is V30() real ext-real Element of REAL
(exp_R . p) + ((- 1) * (exp_R . ((- 1) * p))) is V30() real ext-real Element of REAL
(diff (exp_R,p)) - (diff ((exp_R * ff),p)) is V30() real ext-real Element of REAL
(exp_R . p) - (diff ((exp_R * ff),p)) is V30() real ext-real Element of REAL
(exp_R . p) - ((- 1) * (exp_R . (ff . p))) is V30() real ext-real Element of REAL
(exp_R . p) - ((- 1) * (exp_R . ((- 1) * p))) is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R - (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R - (exp_R * ff)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
diff (((1 / 2) (#) (exp_R - (exp_R * ff))),p) is V30() real ext-real Element of REAL
diff ((exp_R - (exp_R * ff)),p) is V30() real ext-real Element of REAL
(1 / 2) * (diff ((exp_R - (exp_R * ff)),p)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R - (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R - (exp_R * ff)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((1 / 2) (#) (exp_R - (exp_R * ff))) . p is V30() real ext-real Element of REAL
dom (exp_R - (exp_R * ff)) is V52() V53() V54() Element of K19(REAL)
dom (exp_R * ff) is V52() V53() V54() Element of K19(REAL)
(dom exp_R) /\ (dom (exp_R * ff)) is V52() V53() V54() Element of K19(REAL)
dom ((1 / 2) (#) (exp_R - (exp_R * ff))) is V52() V53() V54() Element of K19(REAL)
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
exp_R . ((- 1) * p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . ((- 1) * p)) is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R . p) - (exp_R . ((- 1) * p))) is V30() real ext-real Element of REAL
(exp_R * ff) . p is V30() real ext-real Element of REAL
(exp_R . p) - ((exp_R * ff) . p) is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R . p) - ((exp_R * ff) . p)) is V30() real ext-real Element of REAL
(exp_R - (exp_R * ff)) . p is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R - (exp_R * ff)) . p) is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * p is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R - (exp_R * p) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R - (exp_R * p)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((1 / 2) (#) (exp_R - (exp_R * p))) is V52() V53() V54() Element of K19(REAL)
ff is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
((1 / 2) (#) (exp_R - (exp_R * p))) . ff is V30() real ext-real Element of REAL
p is V30() real ext-real set
diff ((),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
exp_R * compreal is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R - (exp_R * compreal) is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R - (exp_R * compreal)) is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
diff (((1 / 2) (#) (exp_R - (exp_R * compreal))),p) is V30() real ext-real Element of REAL
diff ((exp_R - (exp_R * compreal)),p) is V30() real ext-real Element of REAL
(1 / 2) * (diff ((exp_R - (exp_R * compreal)),p)) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R + (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R + (exp_R * ff)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) is V30() real ext-real Element of REAL
diff ((exp_R + (exp_R * ff)),p) is V30() real ext-real Element of REAL
(1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) is V30() real ext-real Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R + (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R + (exp_R * ff)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((1 / 2) (#) (exp_R + (exp_R * ff))) . p is V30() real ext-real Element of REAL
dom (exp_R + (exp_R * ff)) is V52() V53() V54() Element of K19(REAL)
dom (exp_R * ff) is V52() V53() V54() Element of K19(REAL)
(dom exp_R) /\ (dom (exp_R * ff)) is V52() V53() V54() Element of K19(REAL)
dom ((1 / 2) (#) (exp_R + (exp_R * ff))) is V52() V53() V54() Element of K19(REAL)
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
(- 1) * p is V30() real ext-real Element of REAL
exp_R . ((- 1) * p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . ((- 1) * p)) is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R . p) + (exp_R . ((- 1) * p))) is V30() real ext-real Element of REAL
(exp_R * ff) . p is V30() real ext-real Element of REAL
(exp_R . p) + ((exp_R * ff) . p) is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R . p) + ((exp_R * ff) . p)) is V30() real ext-real Element of REAL
(exp_R + (exp_R * ff)) . p is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R + (exp_R * ff)) . p) is V30() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * p is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R + (exp_R * p) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R + (exp_R * p)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((1 / 2) (#) (exp_R + (exp_R * p))) is V52() V53() V54() Element of K19(REAL)
ff is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
((1 / 2) (#) (exp_R + (exp_R * p))) . ff is V30() real ext-real Element of REAL
p is V30() real ext-real set
diff ((),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R * ff is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
exp_R + (exp_R * ff) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / 2) (#) (exp_R + (exp_R * ff)) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) is V30() real ext-real Element of REAL
diff ((exp_R + (exp_R * ff)),p) is V30() real ext-real Element of REAL
(1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
(1 / 2) * ((exp_R . p) - (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
() / () is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real set
diff ((() / ()),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
1 / ((() . p) ^2) is V30() real ext-real Element of REAL
diff ((),p) is V30() real ext-real Element of REAL
(diff ((),p)) * (() . p) is V30() real ext-real Element of REAL
diff ((),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(diff ((),p)) * (() . p) is V30() real ext-real Element of REAL
((diff ((),p)) * (() . p)) - ((diff ((),p)) * (() . p)) is V30() real ext-real Element of REAL
(((diff ((),p)) * (() . p)) - ((diff ((),p)) * (() . p))) / ((() . p) ^2) is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real Element of REAL
((() . p) * (() . p)) - ((diff ((),p)) * (() . p)) is V30() real ext-real Element of REAL
(((() . p) * (() . p)) - ((diff ((),p)) * (() . p))) / ((() . p) ^2) is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real Element of REAL
((() . p) ^2) - ((() . p) * (() . p)) is V30() real ext-real Element of REAL
(((() . p) ^2) - ((() . p) * (() . p))) / ((() . p) ^2) is V30() real ext-real Element of REAL
rng () is V52() V53() V54() Element of K19(REAL)
p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
dom (() / ()) is V52() V53() V54() Element of K19(REAL)
() " {0} is V52() V53() V54() Element of K19(REAL)
(dom ()) \ (() " {0}) is V52() V53() V54() Element of K19(REAL)
(dom ()) /\ ((dom ()) \ (() " {0})) is V52() V53() V54() Element of K19(REAL)
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
(() / ()) . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) " is V30() real ext-real Element of REAL
(() . p) * ((() . p) ") is V30() real ext-real Element of REAL
(() . p) / (() . p) is V30() real ext-real Element of REAL
p is V30() real ext-real set
ff is V30() real ext-real set
diff ((),ff) is V30() real ext-real Element of REAL
() . ff is V30() real ext-real Element of REAL
(() . ff) ^2 is V30() real ext-real Element of REAL
(() . ff) * (() . ff) is V30() real ext-real set
1 / ((() . ff) ^2) is V30() real ext-real Element of REAL
p is V30() real ext-real set
diff ((),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
[#] REAL is closed open V52() V53() V54() Element of K19(REAL)
ff is V30() real ext-real Element of REAL
p is V30() real ext-real set
diff ((),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
[#] REAL is closed open V52() V53() V54() Element of K19(REAL)
ff is V30() real ext-real Element of REAL
p is V30() real ext-real set
diff ((),p) is V30() real ext-real Element of REAL
() . p is V30() real ext-real Element of REAL
(() . p) ^2 is V30() real ext-real Element of REAL
(() . p) * (() . p) is V30() real ext-real set
1 / ((() . p) ^2) is V30() real ext-real Element of REAL
[#] REAL is closed open V52() V53() V54() Element of K19(REAL)
ff is V30() real ext-real Element of REAL
p is V30() real ext-real set
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . p) * (exp_R . (- p)) is V30() real ext-real Element of REAL
sqrt ((exp_R . p) * (exp_R . (- p))) is V30() real ext-real Element of REAL
2 * (sqrt ((exp_R . p) * (exp_R . (- p)))) is V30() real ext-real Element of REAL
p + (- p) is V30() real ext-real Element of REAL
exp_R . (p + (- p)) is V30() real ext-real Element of REAL
sqrt (exp_R . (p + (- p))) is V30() real ext-real Element of REAL
2 * (sqrt (exp_R . (p + (- p)))) is V30() real ext-real Element of REAL
2 * 1 is ordinal natural V30() real ext-real non negative Element of REAL
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
2 / 2 is V30() real ext-real non negative Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) / 2 is V30() real ext-real Element of REAL
p is V30() real ext-real set
p is V30() real ext-real set
p is V30() real ext-real set
() | REAL is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
() | REAL is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
() | REAL is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V30() real ext-real set
() . p is V30() real ext-real Element of REAL
exp_R . p is V30() real ext-real Element of REAL
- p is V30() real ext-real Element of REAL
exp_R . (- p) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
1 * ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . p) + (exp_R . (- p))) - (exp_R . p) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) - (exp_R . p) is V30() real ext-real Element of REAL
(exp_R . (- p)) + (exp_R . (- p)) is V30() real ext-real Element of REAL
- (exp_R . (- p)) is V30() real ext-real Element of REAL
(- (exp_R . (- p))) + (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . p) - (exp_R . (- p)) is V30() real ext-real Element of REAL
(exp_R . p) + (exp_R . (- p)) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
(((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
(- 1) * ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
- ((exp_R . p) + (exp_R . (- p))) is V30() real ext-real Element of REAL
((exp_R . p) - (exp_R . (- p))) + (exp_R . (- p)) is V30() real ext-real Element of REAL
- (exp_R . p) is V30() real ext-real Element of REAL
- (exp_R . (- p)) is V30() real ext-real Element of REAL
(- (exp_R . p)) + (- (exp_R . (- p))) is V30() real ext-real Element of REAL
((- (exp_R . p)) + (- (exp_R . (- p)))) + (exp_R . (- p)) is V30() real ext-real Element of REAL