REAL is non empty V51() V52() V53() V57() V62() set
NAT is non empty V21() V22() V23() V51() V52() V53() V54() V55() V56() V57() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V51() V57() V62() set
K20(NAT,REAL) is Relation-like V34() V35() V36() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is Relation-like V34() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is Relation-like V34() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(REAL,REAL) is Relation-like V34() V35() V36() set
K19(K20(REAL,REAL)) is set
PFuncs (REAL,REAL) is set
K20(NAT,(PFuncs (REAL,REAL))) is Relation-like set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
ExtREAL is non empty V52() set
RAT is non empty V51() V52() V53() V54() V57() V62() set
INT is non empty V51() V52() V53() V54() V55() V57() V62() set
NAT is non empty V21() V22() V23() V51() V52() V53() V54() V55() V56() V57() set
K19(NAT) is set
K19(NAT) is set
K20(COMPLEX,REAL) is Relation-like V34() V35() V36() set
K19(K20(COMPLEX,REAL)) is set
{} is set
the Relation-like non-empty empty-yielding RAT -valued empty V21() V22() V23() V25() V26() V27() V29() V30() non negative V34() V35() V36() V37() V51() V52() V53() V54() V55() V56() V57() set is Relation-like non-empty empty-yielding RAT -valued empty V21() V22() V23() V25() V26() V27() V29() V30() non negative V34() V35() V36() V37() V51() V52() V53() V54() V55() V56() V57() set
1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
{{},1} is set
0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
tan is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
cos is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin / cos is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom tan is set
cot is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos / sin is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom cot is set
K405(REAL,sin) is non empty V51() V52() V53() Element of K19(REAL)
K405(REAL,cos) is non empty V51() V52() V53() Element of K19(REAL)
cos . 0 is V28() V29() ext-real Element of REAL
sin . 0 is V28() V29() ext-real Element of REAL
cos 0 is V28() V29() ext-real Element of REAL
sin 0 is V28() V29() ext-real Element of REAL
PI is V28() V29() ext-real Element of REAL
2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
PI / 2 is V28() V29() ext-real Element of REAL
cos . (PI / 2) is V28() V29() ext-real Element of REAL
sin . (PI / 2) is V28() V29() ext-real Element of REAL
cos . PI is V28() V29() ext-real Element of REAL
- 1 is V28() V29() V30() ext-real Element of REAL
sin . PI is V28() V29() ext-real Element of REAL
PI + (PI / 2) is V28() V29() ext-real Element of REAL
cos . (PI + (PI / 2)) is V28() V29() ext-real Element of REAL
sin . (PI + (PI / 2)) is V28() V29() ext-real Element of REAL
2 * PI is V28() V29() ext-real Element of REAL
cos . (2 * PI) is V28() V29() ext-real Element of REAL
sin . (2 * PI) is V28() V29() ext-real Element of REAL
cos ^ is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin ^ is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * sin is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * sin) is set
sinh is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
cosh is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
arcsin is Relation-like V6() V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
#Z 2 is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z 2) * arcsin is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / 2 is V28() V29() ext-real Element of REAL
(1 / 2) (#) ((#Z 2) * arcsin) is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K405(REAL,((1 / 2) (#) ((#Z 2) * arcsin))) is V51() V52() V53() Element of K19(REAL)
].(- 1),1.[ is V51() V52() V53() open Element of K19(REAL)
arccos is Relation-like V6() V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
(#Z 2) * arccos is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(1 / 2) (#) ((#Z 2) * arccos) is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K405(REAL,((1 / 2) (#) ((#Z 2) * arccos))) is V51() V52() V53() Element of K19(REAL)
#R (1 / 2) is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K405(REAL,tan) is V51() V52() V53() Element of K19(REAL)
K405(REAL,cot) is V51() V52() V53() Element of K19(REAL)
sec is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K405(REAL,sec) is V51() V52() V53() Element of K19(REAL)
cosec is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K405(REAL,cosec) is V51() V52() V53() Element of K19(REAL)
- cosec is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) is V28() V29() V30() set
K98(1) (#) cosec is Relation-like V6() V34() V35() V36() set
arctan is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
[.(- 1),1.] is non empty V51() V52() V53() closed Element of K19(REAL)
arctan | [.(- 1),1.] is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
arccot is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
arccot | [.(- 1),1.] is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
[#] REAL is V51() V52() V53() closed open Element of K19(REAL)
AffineMap ((1 / 2),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
dom (AffineMap ((1 / 2),0)) is non empty set
AffineMap (2,0) is Relation-like V6() V7() non empty total V18( REAL , REAL ) V19( REAL ) V20( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap (2,0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
dom (sin * (AffineMap (2,0))) is non empty set
4 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
1 / 4 is V28() V29() ext-real Element of REAL
(1 / 4) (#) (sin * (AffineMap (2,0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
dom ((1 / 4) (#) (sin * (AffineMap (2,0)))) is non empty set
(AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0)))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
- ((1 / 4) (#) (sin * (AffineMap (2,0)))) is Relation-like V6() V34() V35() V36() set
K98(1) (#) ((1 / 4) (#) (sin * (AffineMap (2,0)))) is Relation-like V6() V34() V35() V36() set
(AffineMap ((1 / 2),0)) + (- ((1 / 4) (#) (sin * (AffineMap (2,0))))) is Relation-like V6() V34() V35() V36() set
((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V28() V29() ext-real Element of REAL
(AffineMap (2,0)) . A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
(2 * A) + 0 is V28() V29() ext-real Element of REAL
dom ((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) is non empty set
A is V28() V29() ext-real Element of REAL
(AffineMap ((1 / 2),0)) . A is V28() V29() ext-real Element of REAL
(1 / 2) * A is V28() V29() ext-real Element of REAL
((1 / 2) * A) + 0 is V28() V29() ext-real Element of REAL
((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V28() V29() ext-real Element of REAL
(((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
cos (2 * A) is V28() V29() ext-real Element of REAL
cos . (2 * A) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos (2 * A)) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap (2,0))),A) is V28() V29() ext-real Element of REAL
(1 / 4) * (diff ((sin * (AffineMap (2,0))),A)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap (2,0))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap (2,0))) `| REAL) . A is V28() V29() ext-real Element of REAL
(1 / 4) * (((sin * (AffineMap (2,0))) `| REAL) . A) is V28() V29() ext-real Element of REAL
(2 * A) + 0 is V28() V29() ext-real Element of REAL
cos . ((2 * A) + 0) is V28() V29() ext-real Element of REAL
2 * (cos . ((2 * A) + 0)) is V28() V29() ext-real Element of REAL
(1 / 4) * (2 * (cos . ((2 * A) + 0))) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
(((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . A is V28() V29() ext-real Element of REAL
sin . A is V28() V29() ext-real Element of REAL
(sin . A) ^2 is V28() V29() ext-real Element of REAL
K97((sin . A),(sin . A)) is set
diff ((AffineMap ((1 / 2),0)),A) is V28() V29() ext-real Element of REAL
diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A) is V28() V29() ext-real Element of REAL
(diff ((AffineMap ((1 / 2),0)),A)) - (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A)) is V28() V29() ext-real Element of REAL
(AffineMap ((1 / 2),0)) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((AffineMap ((1 / 2),0)) `| REAL) . A is V28() V29() ext-real Element of REAL
(((AffineMap ((1 / 2),0)) `| REAL) . A) - (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A)) is V28() V29() ext-real Element of REAL
(1 / 2) - (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A)) is V28() V29() ext-real Element of REAL
(((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . A is V28() V29() ext-real Element of REAL
(1 / 2) - ((((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . A) is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
cos (2 * A) is V28() V29() ext-real Element of REAL
cos . (2 * A) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos (2 * A)) is V28() V29() ext-real Element of REAL
(1 / 2) - ((1 / 2) * (cos (2 * A))) is V28() V29() ext-real Element of REAL
1 - (cos (2 * A)) is V28() V29() ext-real Element of REAL
(1 - (cos (2 * A))) / 2 is V28() V29() ext-real Element of REAL
sin A is V28() V29() ext-real Element of REAL
(sin A) ^2 is V28() V29() ext-real Element of REAL
K97((sin A),(sin A)) is set
A is V28() V29() ext-real Element of REAL
(((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . A is V28() V29() ext-real Element of REAL
sin . A is V28() V29() ext-real Element of REAL
(sin . A) ^2 is V28() V29() ext-real Element of REAL
K97((sin . A),(sin . A)) is set
(AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0)))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V28() V29() ext-real Element of REAL
(AffineMap (2,0)) . A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
(2 * A) + 0 is V28() V29() ext-real Element of REAL
dom ((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) is non empty set
A is V28() V29() ext-real Element of REAL
(AffineMap ((1 / 2),0)) . A is V28() V29() ext-real Element of REAL
(1 / 2) * A is V28() V29() ext-real Element of REAL
((1 / 2) * A) + 0 is V28() V29() ext-real Element of REAL
((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V28() V29() ext-real Element of REAL
(((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
cos (2 * A) is V28() V29() ext-real Element of REAL
cos . (2 * A) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos (2 * A)) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap (2,0))),A) is V28() V29() ext-real Element of REAL
(1 / 4) * (diff ((sin * (AffineMap (2,0))),A)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap (2,0))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap (2,0))) `| REAL) . A is V28() V29() ext-real Element of REAL
(1 / 4) * (((sin * (AffineMap (2,0))) `| REAL) . A) is V28() V29() ext-real Element of REAL
(2 * A) + 0 is V28() V29() ext-real Element of REAL
cos . ((2 * A) + 0) is V28() V29() ext-real Element of REAL
2 * (cos . ((2 * A) + 0)) is V28() V29() ext-real Element of REAL
(1 / 4) * (2 * (cos . ((2 * A) + 0))) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
(((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . A is V28() V29() ext-real Element of REAL
cos . A is V28() V29() ext-real Element of REAL
(cos . A) ^2 is V28() V29() ext-real Element of REAL
K97((cos . A),(cos . A)) is set
diff ((AffineMap ((1 / 2),0)),A) is V28() V29() ext-real Element of REAL
diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A) is V28() V29() ext-real Element of REAL
(diff ((AffineMap ((1 / 2),0)),A)) + (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A)) is V28() V29() ext-real Element of REAL
(AffineMap ((1 / 2),0)) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((AffineMap ((1 / 2),0)) `| REAL) . A is V28() V29() ext-real Element of REAL
(((AffineMap ((1 / 2),0)) `| REAL) . A) + (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A)) is V28() V29() ext-real Element of REAL
(1 / 2) + (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),A)) is V28() V29() ext-real Element of REAL
(((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . A is V28() V29() ext-real Element of REAL
(1 / 2) + ((((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . A) is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
cos (2 * A) is V28() V29() ext-real Element of REAL
cos . (2 * A) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos (2 * A)) is V28() V29() ext-real Element of REAL
(1 / 2) + ((1 / 2) * (cos (2 * A))) is V28() V29() ext-real Element of REAL
1 + (cos (2 * A)) is V28() V29() ext-real Element of REAL
(1 + (cos (2 * A))) / 2 is V28() V29() ext-real Element of REAL
cos A is V28() V29() ext-real Element of REAL
(cos A) ^2 is V28() V29() ext-real Element of REAL
K97((cos A),(cos A)) is set
A is V28() V29() ext-real Element of REAL
(((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . A is V28() V29() ext-real Element of REAL
cos . A is V28() V29() ext-real Element of REAL
(cos . A) ^2 is V28() V29() ext-real Element of REAL
K97((cos . A),(cos . A)) is set
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
A + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
#Z (A + 1) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z (A + 1)) * sin is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / (A + 1) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) (#) ((#Z (A + 1)) * sin) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((1 / (A + 1)) (#) ((#Z (A + 1)) * sin)) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((1 / (A + 1)) (#) ((#Z (A + 1)) * sin)) is non empty set
Z is V28() V29() ext-real Element of REAL
dom ((#Z (A + 1)) * sin) is non empty set
Z is V28() V29() ext-real Element of REAL
((#Z (A + 1)) * sin) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f2 is V28() V29() ext-real Element of REAL
(((#Z (A + 1)) * sin) `| REAL) . f2 is V28() V29() ext-real Element of REAL
sin . f2 is V28() V29() ext-real Element of REAL
(sin . f2) #Z A is V28() V29() ext-real Element of REAL
(A + 1) * ((sin . f2) #Z A) is V28() V29() ext-real Element of REAL
cos . f2 is V28() V29() ext-real Element of REAL
((A + 1) * ((sin . f2) #Z A)) * (cos . f2) is V28() V29() ext-real Element of REAL
diff (((#Z (A + 1)) * sin),f2) is V28() V29() ext-real Element of REAL
(A + 1) - 1 is V28() V29() V30() ext-real Element of REAL
(sin . f2) #Z ((A + 1) - 1) is V28() V29() ext-real Element of REAL
(A + 1) * ((sin . f2) #Z ((A + 1) - 1)) is V28() V29() ext-real Element of REAL
diff (sin,f2) is V28() V29() ext-real Element of REAL
((A + 1) * ((sin . f2) #Z ((A + 1) - 1))) * (diff (sin,f2)) is V28() V29() ext-real Element of REAL
((A + 1) * ((sin . f2) #Z ((A + 1) - 1))) * (cos . f2) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) (#) ((#Z (A + 1)) * sin)) `| REAL) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(sin . Z) #Z A is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
((sin . Z) #Z A) * (cos . Z) is V28() V29() ext-real Element of REAL
diff (((#Z (A + 1)) * sin),Z) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (diff (((#Z (A + 1)) * sin),Z)) is V28() V29() ext-real Element of REAL
(((#Z (A + 1)) * sin) `| REAL) . Z is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * ((((#Z (A + 1)) * sin) `| REAL) . Z) is V28() V29() ext-real Element of REAL
(A + 1) * ((sin . Z) #Z A) is V28() V29() ext-real Element of REAL
((A + 1) * ((sin . Z) #Z A)) * (cos . Z) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (((A + 1) * ((sin . Z) #Z A)) * (cos . Z)) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (A + 1) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) * (A + 1)) * ((sin . Z) #Z A) is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) * (A + 1)) * ((sin . Z) #Z A)) * (cos . Z) is V28() V29() ext-real Element of REAL
(A + 1) / (A + 1) is V28() V29() ext-real Element of REAL
((A + 1) / (A + 1)) * ((sin . Z) #Z A) is V28() V29() ext-real Element of REAL
(((A + 1) / (A + 1)) * ((sin . Z) #Z A)) * (cos . Z) is V28() V29() ext-real Element of REAL
1 * ((sin . Z) #Z A) is V28() V29() ext-real Element of REAL
(1 * ((sin . Z) #Z A)) * (cos . Z) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) (#) ((#Z (A + 1)) * sin)) `| REAL) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(sin . Z) #Z A is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
((sin . Z) #Z A) * (cos . Z) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
A + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
#Z (A + 1) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z (A + 1)) * cos is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / (A + 1) is V28() V29() ext-real Element of REAL
- (1 / (A + 1)) is V28() V29() ext-real Element of REAL
(- (1 / (A + 1))) (#) ((#Z (A + 1)) * cos) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (1 / (A + 1))) (#) ((#Z (A + 1)) * cos)) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (1 / (A + 1))) (#) ((#Z (A + 1)) * cos)) is non empty set
Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
dom (#Z (A + 1)) is non empty set
dom ((#Z (A + 1)) * cos) is non empty set
((#Z (A + 1)) * cos) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (A + 1) is V28() V29() V30() ext-real Element of REAL
f2 is V28() V29() ext-real Element of REAL
(((#Z (A + 1)) * cos) `| REAL) . f2 is V28() V29() ext-real Element of REAL
cos . f2 is V28() V29() ext-real Element of REAL
(cos . f2) #Z A is V28() V29() ext-real Element of REAL
(- (A + 1)) * ((cos . f2) #Z A) is V28() V29() ext-real Element of REAL
sin . f2 is V28() V29() ext-real Element of REAL
((- (A + 1)) * ((cos . f2) #Z A)) * (sin . f2) is V28() V29() ext-real Element of REAL
diff (((#Z (A + 1)) * cos),f2) is V28() V29() ext-real Element of REAL
(A + 1) - 1 is V28() V29() V30() ext-real Element of REAL
(cos . f2) #Z ((A + 1) - 1) is V28() V29() ext-real Element of REAL
(A + 1) * ((cos . f2) #Z ((A + 1) - 1)) is V28() V29() ext-real Element of REAL
diff (cos,f2) is V28() V29() ext-real Element of REAL
((A + 1) * ((cos . f2) #Z ((A + 1) - 1))) * (diff (cos,f2)) is V28() V29() ext-real Element of REAL
- (sin . f2) is V28() V29() ext-real Element of REAL
((A + 1) * ((cos . f2) #Z ((A + 1) - 1))) * (- (sin . f2)) is V28() V29() ext-real Element of REAL
(- (A + 1)) * ((cos . f2) #Z ((A + 1) - 1)) is V28() V29() ext-real Element of REAL
((- (A + 1)) * ((cos . f2) #Z ((A + 1) - 1))) * (sin . f2) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(((- (1 / (A + 1))) (#) ((#Z (A + 1)) * cos)) `| REAL) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
(cos . Z) #Z A is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
((cos . Z) #Z A) * (sin . Z) is V28() V29() ext-real Element of REAL
diff (((#Z (A + 1)) * cos),Z) is V28() V29() ext-real Element of REAL
(- (1 / (A + 1))) * (diff (((#Z (A + 1)) * cos),Z)) is V28() V29() ext-real Element of REAL
(((#Z (A + 1)) * cos) `| REAL) . Z is V28() V29() ext-real Element of REAL
(- (1 / (A + 1))) * ((((#Z (A + 1)) * cos) `| REAL) . Z) is V28() V29() ext-real Element of REAL
(- (A + 1)) * ((cos . Z) #Z A) is V28() V29() ext-real Element of REAL
((- (A + 1)) * ((cos . Z) #Z A)) * (sin . Z) is V28() V29() ext-real Element of REAL
(- (1 / (A + 1))) * (((- (A + 1)) * ((cos . Z) #Z A)) * (sin . Z)) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (A + 1) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) * (A + 1)) * ((cos . Z) #Z A) is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) * (A + 1)) * ((cos . Z) #Z A)) * (sin . Z) is V28() V29() ext-real Element of REAL
(A + 1) / (A + 1) is V28() V29() ext-real Element of REAL
((A + 1) / (A + 1)) * ((cos . Z) #Z A) is V28() V29() ext-real Element of REAL
(((A + 1) / (A + 1)) * ((cos . Z) #Z A)) * (sin . Z) is V28() V29() ext-real Element of REAL
1 * ((cos . Z) #Z A) is V28() V29() ext-real Element of REAL
(1 * ((cos . Z) #Z A)) * (sin . Z) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(((- (1 / (A + 1))) (#) ((#Z (A + 1)) * cos)) `| REAL) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
(cos . Z) #Z A is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
((cos . Z) #Z A) * (sin . Z) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
Z is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
A + Z is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
A - Z is V28() V29() V30() ext-real Element of REAL
AffineMap ((A + Z),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap ((A + Z),0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
2 * (A + Z) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
1 / (2 * (A + Z)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
AffineMap ((A - Z),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap ((A - Z),0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
2 * (A - Z) is V28() V29() V30() ext-real Element of REAL
1 / (2 * (A - Z)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) + ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
(((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) + ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0))))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sin * (AffineMap ((A - Z),0))) is non empty set
f2 is V28() V29() ext-real Element of REAL
(AffineMap ((A - Z),0)) . f2 is V28() V29() ext-real Element of REAL
(A - Z) * f2 is V28() V29() ext-real Element of REAL
((A - Z) * f2) + 0 is V28() V29() ext-real Element of REAL
dom ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) is non empty set
((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f2 is V28() V29() ext-real Element of REAL
(((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(A - Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A - Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A - Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A - Z) * f2)) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap ((A - Z),0))),f2) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) * (diff ((sin * (AffineMap ((A - Z),0))),f2)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap ((A - Z),0))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap ((A - Z),0))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) * (((sin * (AffineMap ((A - Z),0))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
((A - Z) * f2) + 0 is V28() V29() ext-real Element of REAL
cos . (((A - Z) * f2) + 0) is V28() V29() ext-real Element of REAL
(A - Z) * (cos . (((A - Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) * ((A - Z) * (cos . (((A - Z) * f2) + 0))) is V28() V29() ext-real Element of REAL
(A - Z) * (1 / (2 * (A - Z))) is V28() V29() ext-real Element of REAL
((A - Z) * (1 / (2 * (A - Z)))) * (cos . (((A - Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
1 * (A - Z) is V28() V29() V30() ext-real Element of REAL
(1 * (A - Z)) / (2 * (A - Z)) is V28() V29() ext-real Element of REAL
((1 * (A - Z)) / (2 * (A - Z))) * (cos . (((A - Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
dom (((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) + ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0))))) is non empty set
dom (sin * (AffineMap ((A + Z),0))) is non empty set
f2 is V28() V29() ext-real Element of REAL
(AffineMap ((A + Z),0)) . f2 is V28() V29() ext-real Element of REAL
(A + Z) * f2 is V28() V29() ext-real Element of REAL
((A + Z) * f2) + 0 is V28() V29() ext-real Element of REAL
dom ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) is non empty set
((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f2 is V28() V29() ext-real Element of REAL
(((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(A + Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A + Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A + Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A + Z) * f2)) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap ((A + Z),0))),f2) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) * (diff ((sin * (AffineMap ((A + Z),0))),f2)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap ((A + Z),0))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap ((A + Z),0))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) * (((sin * (AffineMap ((A + Z),0))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
((A + Z) * f2) + 0 is V28() V29() ext-real Element of REAL
cos . (((A + Z) * f2) + 0) is V28() V29() ext-real Element of REAL
(A + Z) * (cos . (((A + Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) * ((A + Z) * (cos . (((A + Z) * f2) + 0))) is V28() V29() ext-real Element of REAL
(A + Z) * (1 / (2 * (A + Z))) is V28() V29() ext-real Element of REAL
((A + Z) * (1 / (2 * (A + Z)))) * (cos . (((A + Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
1 * (A + Z) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
(1 * (A + Z)) / (2 * (A + Z)) is V28() V29() ext-real Element of REAL
((1 * (A + Z)) / (2 * (A + Z))) * (cos . (((A + Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) + ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0))))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
A * f2 is V28() V29() ext-real Element of REAL
cos . (A * f2) is V28() V29() ext-real Element of REAL
Z * f2 is V28() V29() ext-real Element of REAL
cos . (Z * f2) is V28() V29() ext-real Element of REAL
(cos . (A * f2)) * (cos . (Z * f2)) is V28() V29() ext-real Element of REAL
diff (((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))),f2) is V28() V29() ext-real Element of REAL
diff (((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))),f2) is V28() V29() ext-real Element of REAL
(diff (((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))),f2)) + (diff (((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))),f2)) is V28() V29() ext-real Element of REAL
(((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2) + (diff (((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))),f2)) is V28() V29() ext-real Element of REAL
(((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2) + ((((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
(A + Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A + Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A + Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A + Z) * f2)) is V28() V29() ext-real Element of REAL
((1 / 2) * (cos ((A + Z) * f2))) + ((((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
(A - Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A - Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A - Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A - Z) * f2)) is V28() V29() ext-real Element of REAL
((1 / 2) * (cos ((A + Z) * f2))) + ((1 / 2) * (cos ((A - Z) * f2))) is V28() V29() ext-real Element of REAL
(cos ((A + Z) * f2)) + (cos ((A - Z) * f2)) is V28() V29() ext-real Element of REAL
(1 / 2) * ((cos ((A + Z) * f2)) + (cos ((A - Z) * f2))) is V28() V29() ext-real Element of REAL
((A + Z) * f2) + ((A - Z) * f2) is V28() V29() ext-real Element of REAL
(((A + Z) * f2) + ((A - Z) * f2)) / 2 is V28() V29() ext-real Element of REAL
cos ((((A + Z) * f2) + ((A - Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
cos . ((((A + Z) * f2) + ((A - Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
((A + Z) * f2) - ((A - Z) * f2) is V28() V29() ext-real Element of REAL
(((A + Z) * f2) - ((A - Z) * f2)) / 2 is V28() V29() ext-real Element of REAL
cos ((((A + Z) * f2) - ((A - Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
cos . ((((A + Z) * f2) - ((A - Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
(cos ((((A + Z) * f2) + ((A - Z) * f2)) / 2)) * (cos ((((A + Z) * f2) - ((A - Z) * f2)) / 2)) is V28() V29() ext-real Element of REAL
2 * ((cos ((((A + Z) * f2) + ((A - Z) * f2)) / 2)) * (cos ((((A + Z) * f2) - ((A - Z) * f2)) / 2))) is V28() V29() ext-real Element of REAL
(1 / 2) * (2 * ((cos ((((A + Z) * f2) + ((A - Z) * f2)) / 2)) * (cos ((((A + Z) * f2) - ((A - Z) * f2)) / 2)))) is V28() V29() ext-real Element of REAL
f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) + ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0))))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
A * f2 is V28() V29() ext-real Element of REAL
cos . (A * f2) is V28() V29() ext-real Element of REAL
Z * f2 is V28() V29() ext-real Element of REAL
cos . (Z * f2) is V28() V29() ext-real Element of REAL
(cos . (A * f2)) * (cos . (Z * f2)) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
Z is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
A + Z is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
A - Z is V28() V29() V30() ext-real Element of REAL
AffineMap ((A - Z),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap ((A - Z),0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
2 * (A - Z) is V28() V29() V30() ext-real Element of REAL
1 / (2 * (A - Z)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
AffineMap ((A + Z),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap ((A + Z),0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
2 * (A + Z) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
1 / (2 * (A + Z)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) - ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
- ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) is Relation-like V6() V34() V35() V36() set
K98(1) (#) ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) is Relation-like V6() V34() V35() V36() set
((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) + (- ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))))) is Relation-like V6() V34() V35() V36() set
(((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) - ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) is non empty set
dom (sin * (AffineMap ((A - Z),0))) is non empty set
f2 is V28() V29() ext-real Element of REAL
(AffineMap ((A - Z),0)) . f2 is V28() V29() ext-real Element of REAL
(A - Z) * f2 is V28() V29() ext-real Element of REAL
((A - Z) * f2) + 0 is V28() V29() ext-real Element of REAL
((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f2 is V28() V29() ext-real Element of REAL
(((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(A - Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A - Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A - Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A - Z) * f2)) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap ((A - Z),0))),f2) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) * (diff ((sin * (AffineMap ((A - Z),0))),f2)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap ((A - Z),0))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap ((A - Z),0))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) * (((sin * (AffineMap ((A - Z),0))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
((A - Z) * f2) + 0 is V28() V29() ext-real Element of REAL
cos . (((A - Z) * f2) + 0) is V28() V29() ext-real Element of REAL
(A - Z) * (cos . (((A - Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) * ((A - Z) * (cos . (((A - Z) * f2) + 0))) is V28() V29() ext-real Element of REAL
(A - Z) * (1 / (2 * (A - Z))) is V28() V29() ext-real Element of REAL
((A - Z) * (1 / (2 * (A - Z)))) * (cos . (((A - Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
1 * (A - Z) is V28() V29() V30() ext-real Element of REAL
(1 * (A - Z)) / (2 * (A - Z)) is V28() V29() ext-real Element of REAL
((1 * (A - Z)) / (2 * (A - Z))) * (cos . (((A - Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
dom (((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) - ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))))) is non empty set
dom (sin * (AffineMap ((A + Z),0))) is non empty set
f2 is V28() V29() ext-real Element of REAL
(AffineMap ((A + Z),0)) . f2 is V28() V29() ext-real Element of REAL
(A + Z) * f2 is V28() V29() ext-real Element of REAL
((A + Z) * f2) + 0 is V28() V29() ext-real Element of REAL
dom ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) is non empty set
((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f2 is V28() V29() ext-real Element of REAL
(((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(A + Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A + Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A + Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A + Z) * f2)) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap ((A + Z),0))),f2) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) * (diff ((sin * (AffineMap ((A + Z),0))),f2)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap ((A + Z),0))) `| REAL is Relation-like V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap ((A + Z),0))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) * (((sin * (AffineMap ((A + Z),0))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
((A + Z) * f2) + 0 is V28() V29() ext-real Element of REAL
cos . (((A + Z) * f2) + 0) is V28() V29() ext-real Element of REAL
(A + Z) * (cos . (((A + Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) * ((A + Z) * (cos . (((A + Z) * f2) + 0))) is V28() V29() ext-real Element of REAL
(A + Z) * (1 / (2 * (A + Z))) is V28() V29() ext-real Element of REAL
((A + Z) * (1 / (2 * (A + Z)))) * (cos . (((A + Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
1 * (A + Z) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
(1 * (A + Z)) / (2 * (A + Z)) is V28() V29() ext-real Element of REAL
((1 * (A + Z)) / (2 * (A + Z))) * (cos . (((A + Z) * f2) + 0)) is V28() V29() ext-real Element of REAL
f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) - ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
A * f2 is V28() V29() ext-real Element of REAL
sin . (A * f2) is V28() V29() ext-real Element of REAL
Z * f2 is V28() V29() ext-real Element of REAL
sin . (Z * f2) is V28() V29() ext-real Element of REAL
(sin . (A * f2)) * (sin . (Z * f2)) is V28() V29() ext-real Element of REAL
diff (((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))),f2) is V28() V29() ext-real Element of REAL
diff (((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))),f2) is V28() V29() ext-real Element of REAL
(diff (((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))),f2)) - (diff (((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))),f2)) is V28() V29() ext-real Element of REAL
(((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2) - (diff (((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))),f2)) is V28() V29() ext-real Element of REAL
(((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) `| REAL) . f2) - ((((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
(A - Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A - Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A - Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A - Z) * f2)) is V28() V29() ext-real Element of REAL
((1 / 2) * (cos ((A - Z) * f2))) - ((((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0)))) `| REAL) . f2) is V28() V29() ext-real Element of REAL
(A + Z) * f2 is V28() V29() ext-real Element of REAL
cos ((A + Z) * f2) is V28() V29() ext-real Element of REAL
cos . ((A + Z) * f2) is V28() V29() ext-real Element of REAL
(1 / 2) * (cos ((A + Z) * f2)) is V28() V29() ext-real Element of REAL
((1 / 2) * (cos ((A - Z) * f2))) - ((1 / 2) * (cos ((A + Z) * f2))) is V28() V29() ext-real Element of REAL
(cos ((A - Z) * f2)) - (cos ((A + Z) * f2)) is V28() V29() ext-real Element of REAL
(1 / 2) * ((cos ((A - Z) * f2)) - (cos ((A + Z) * f2))) is V28() V29() ext-real Element of REAL
((A - Z) * f2) + ((A + Z) * f2) is V28() V29() ext-real Element of REAL
(((A - Z) * f2) + ((A + Z) * f2)) / 2 is V28() V29() ext-real Element of REAL
sin ((((A - Z) * f2) + ((A + Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
sin . ((((A - Z) * f2) + ((A + Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
((A - Z) * f2) - ((A + Z) * f2) is V28() V29() ext-real Element of REAL
(((A - Z) * f2) - ((A + Z) * f2)) / 2 is V28() V29() ext-real Element of REAL
sin ((((A - Z) * f2) - ((A + Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
sin . ((((A - Z) * f2) - ((A + Z) * f2)) / 2) is V28() V29() ext-real Element of REAL
(sin ((((A - Z) * f2) + ((A + Z) * f2)) / 2)) * (sin ((((A - Z) * f2) - ((A + Z) * f2)) / 2)) is V28() V29() ext-real Element of REAL
2 * ((sin ((((A - Z) * f2) + ((A + Z) * f2)) / 2)) * (sin ((((A - Z) * f2) - ((A + Z) * f2)) / 2))) is V28() V29() ext-real Element of REAL
- (2 * ((sin ((((A - Z) * f2) + ((A + Z) * f2)) / 2)) * (sin ((((A - Z) * f2) - ((A + Z) * f2)) / 2)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (- (2 * ((sin ((((A - Z) * f2) + ((A + Z) * f2)) / 2)) * (sin ((((A - Z) * f2) - ((A + Z) * f2)) / 2))))) is V28() V29() ext-real Element of REAL
sin (A * f2) is V28() V29() ext-real Element of REAL
- (Z * f2) is V28() V29() ext-real Element of REAL
sin (- (Z * f2)) is V28() V29() ext-real Element of REAL
sin . (- (Z * f2)) is V28() V29() ext-real Element of REAL
(sin (A * f2)) * (sin (- (Z * f2))) is V28() V29() ext-real Element of REAL
2 * ((sin (A * f2)) * (sin (- (Z * f2)))) is V28() V29() ext-real Element of REAL
- (2 * ((sin (A * f2)) * (sin (- (Z * f2))))) is V28() V29() ext-real Element of REAL
(1 / 2) * (- (2 * ((sin (A * f2)) * (sin (- (Z * f2)))))) is V28() V29() ext-real Element of REAL
sin (Z * f2) is V28() V29() ext-real Element of REAL
- (sin (Z * f2)) is V28() V29() ext-real Element of REAL
(sin (A * f2)) * (- (sin (Z * f2))) is V28() V29() ext-real Element of REAL
2 * ((sin (A * f2)) * (- (sin (Z * f2)))) is V28() V29() ext-real Element of REAL
- (2 * ((sin (A * f2)) * (- (sin (Z * f2))))) is V28() V29() ext-real Element of REAL
(1 / 2) * (- (2 * ((sin (A * f2)) * (- (sin (Z * f2)))))) is V28() V29() ext-real Element of REAL
f2 is V28() V29() ext-real Element of REAL
((((1 / (2 * (A - Z))) (#) (sin * (AffineMap ((A - Z),0)))) - ((1 / (2 * (A + Z))) (#) (sin * (AffineMap ((A + Z),0))))) `| REAL) . f2 is V28() V29() ext-real Element of REAL
A * f2 is V28() V29() ext-real Element of REAL
sin . (A * f2) is V28() V29() ext-real Element of REAL
Z * f2 is V28() V29() ext-real Element of REAL
sin . (Z * f2) is V28() V29() ext-real Element of REAL
(sin . (A * f2)) * (sin . (Z * f2)) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
Z is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
A + Z is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
A - Z is V28() V29() V30() ext-real Element of REAL
AffineMap ((A + Z),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
cos * (AffineMap ((A + Z),0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
2 * (A + Z) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
1 / (2 * (A + Z)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A + Z))) (#) (cos * (AffineMap ((A + Z),0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
- ((1 / (2 * (A + Z))) (#) (cos * (AffineMap ((A + Z),0)))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) ((1 / (2 * (A + Z))) (#) (cos * (AffineMap ((A + Z),0)))) is Relation-like V6() V34() V35() V36() set
AffineMap ((A - Z),0) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
cos * (AffineMap ((A - Z),0)) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
2 * (A - Z) is V28() V29() V30() ext-real Element of REAL
1 / (2 * (A - Z)) is V28() V29() ext-real Element of REAL
(1 / (2 * (A - Z))) (#) (cos * (AffineMap ((A - Z),0))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
(- ((1 / (2 * (A + Z))) (#) (cos * (AffineMap ((A + Z),0))))) - ((1 / (2 * (A - Z))) (#) (cos * (AffineMap ((A - Z),0)))) is Relation-like V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
- ((1 / (2 * (A - Z))) (#) (cos * (AffineMap ((A - Z),0)))) is Relation-like V6() V34() V35() V36() set
K98(1) (#) ((1 / (2 * (A - Z))) (#) (cos * (AffineMap ((A - Z),0)))) is Relation-like V6() V34() V35() V36() set
(- ((1 / (2 * (A + Z))) (#) (cos * (AffineMap ((A + Z),0))))) + (- ((1 / (2 * (A - Z))) (#) (cos * (AffineMap ((A - Z),0))))) is Relation-like V6() V34() V35() V36() set
((- ((1 / (2 * (A + Z))) (#) (cos * (