let y, u be PartFunc of REAL,REAL; for Z0 being open Subset of REAL st y is differentiable & ['0,PI'] c= Z0 & Z0 c= dom y & y `| Z0 is continuous & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) holds
for n being Nat holds integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) = ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))
let Z0 be open Subset of REAL; ( y is differentiable & ['0,PI'] c= Z0 & Z0 c= dom y & y `| Z0 is continuous & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) implies for n being Nat holds integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) = ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1))) )
assume A1:
( y is differentiable & ['0,PI'] c= Z0 & Z0 c= dom y & y `| Z0 is continuous & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) )
; for n being Nat holds integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) = ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))
set I = AffineMap (0,1);
let n be Nat; integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) = ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))
A3:
1 / (n + 1) < PI - (1 / (n + 1))
by Lm3;
A4:
[.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[
by Lm3;
A5:
['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).]
by Lm3;
set X = ].0,PI.[;
set Z = ['(1 / (n + 1)),(PI - (1 / (n + 1)))'];
set F = ((u (#) u) (#) sin) (#) cos;
A6:
['0,PI'] = [.0,PI.]
by INTEGRA5:def 3, LmPI;
A7:
].0,PI.[ c= Z0
by A1;
y is_differentiable_on Z0
by A1, FDIFF_1:26;
then A8:
dom (y `| Z0) = Z0
by FDIFF_1:def 7;
A9: dom (u (#) u) =
['0,PI'] /\ ['0,PI']
by A1, VALUED_1:def 4
.=
['0,PI']
;
then A10:
( u (#) u is_differentiable_on ].0,PI.[ & (u (#) u) `| ].0,PI.[ = ((u `| ].0,PI.[) (#) u) + (u (#) (u `| ].0,PI.[)) )
by A1, Th13;
A12:
dom sin = REAL
by FUNCT_2:def 1;
then A13: dom ((u (#) u) (#) sin) =
['0,PI'] /\ REAL
by A9, VALUED_1:def 4
.=
['0,PI']
by XBOOLE_1:28
;
then A14:
].0,PI.[ c= dom ((u (#) u) (#) sin)
by A6, Lm1;
sin is_differentiable_on ].0,PI.[
by FDIFF_1:26, SIN_COS:68;
then A15:
( (u (#) u) (#) sin is_differentiable_on ].0,PI.[ & ((u (#) u) (#) sin) `| ].0,PI.[ = (((u (#) u) `| ].0,PI.[) (#) sin) + ((u (#) u) (#) (sin `| ].0,PI.[)) )
by A10, A14, Th13;
then A16: ((u (#) u) (#) sin) `| ].0,PI.[ =
((2 (#) (u (#) (u `| ].0,PI.[))) (#) sin) + ((u (#) u) (#) (sin `| ].0,PI.[))
by A10, Th9
.=
(((2 (#) u) (#) (u `| ].0,PI.[)) (#) sin) + ((u (#) u) (#) (sin `| ].0,PI.[))
by RFUNCT_1:12
;
dom cos = REAL
by FUNCT_2:def 1;
then dom (((u (#) u) (#) sin) (#) cos) =
['0,PI'] /\ REAL
by A13, VALUED_1:def 4
.=
['0,PI']
by XBOOLE_1:28
;
then A17:
].0,PI.[ c= dom (((u (#) u) (#) sin) (#) cos)
by A6, Lm1;
B17:
cos is_differentiable_on ].0,PI.[
by FDIFF_1:26, SIN_COS:67;
then A18:
( ((u (#) u) (#) sin) (#) cos is_differentiable_on ].0,PI.[ & (((u (#) u) (#) sin) (#) cos) `| ].0,PI.[ = ((((u (#) u) (#) sin) `| ].0,PI.[) (#) cos) + (((u (#) u) (#) sin) (#) (cos `| ].0,PI.[)) )
by A15, A17, Th13;
A19:
(((u (#) u) (#) sin) (#) cos) `| ].0,PI.[ = (((((2 (#) u) (#) (u `| ].0,PI.[)) (#) sin) + ((u (#) u) (#) (sin `| ].0,PI.[))) (#) cos) + (((u (#) u) (#) sin) (#) (cos `| ].0,PI.[))
by A15, A16, A17, B17, Th13;
A20:
( cos is_differentiable_on ].0,PI.[ & cos `| ].0,PI.[ = - (sin | ].0,PI.[) )
by Th8;
( sin is_differentiable_on ].0,PI.[ & sin `| ].0,PI.[ = cos | ].0,PI.[ )
by Th8;
then A27:
((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous
by A1, A19, A20;
A28:
dom ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[) = ].0,PI.[
by A18, FDIFF_1:def 7;
A29:
['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)
by A4, A5, A18, FDIFF_1:def 7;
then A30:
( (((u (#) u) (#) sin) (#) cos) `| ].0,PI.[ is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded )
by A27, INTEGRA5:10, INTEGRA5:11;
then A31:
(((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))) = (integral (((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[),(1 / (n + 1)),(PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))
by A3, A5, A18, Lm3, INTEGRA7:10;
set G = (((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[;
set H = (AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin);
B1:
dom (AffineMap (0,1)) = REAL
by FUNCT_2:def 1;
dom (y (#) y) =
(dom y) /\ (dom y)
by VALUED_1:def 4
.=
dom y
;
then A32: dom ((y (#) y) + (AffineMap (0,1))) =
(dom y) /\ REAL
by B1, VALUED_1:def 1
.=
dom y
by XBOOLE_1:28
;
dom ((y `| Z0) (#) (y `| Z0)) =
Z0 /\ Z0
by A8, VALUED_1:def 4
.=
Z0
;
then B32: dom (((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) =
(dom y) /\ Z0
by A32, VALUED_1:12
.=
Z0
by A1, XBOOLE_1:28
;
then A33:
dom ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) = ].0,PI.[
by A7, RELAT_1:62;
dom (u `| ].0,PI.[) = ].0,PI.[
by A1, FDIFF_1:def 7;
then dom ((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) =
].0,PI.[ /\ ].0,PI.[
by VALUED_1:def 4
.=
].0,PI.[
;
then dom (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) =
].0,PI.[ /\ REAL
by A12, VALUED_1:def 4
.=
].0,PI.[
by XBOOLE_1:28
;
then A34: dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) =
].0,PI.[ /\ REAL
by A12, VALUED_1:def 4
.=
].0,PI.[
by XBOOLE_1:28
;
A35: dom ((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) =
(dom (AffineMap (0,1))) /\ (dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin))
by VALUED_1:12
.=
].0,PI.[
by B1, A34, XBOOLE_1:28
;
((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous
by A1;
then A37:
( ((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] )
by A5, A35, Lm3, INTEGRA5:10, INTEGRA5:11;
A38: dom (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) - ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)) =
].0,PI.[ /\ ].0,PI.[
by A28, A35, VALUED_1:12
.=
].0,PI.[
;
now for t being object st t in dom ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) holds
((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) . t = (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) - ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)) . tlet t be
object ;
( t in dom ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) implies ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) . t = (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) - ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)) . t )assume A39:
t in dom ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[)
;
((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) . t = (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) - ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)) . tthen reconsider x =
t as
Real ;
AA:
(AffineMap (0,1)) . x = (0 * x) + 1
by FCONT_1:def 4;
A41:
(u `| ].0,PI.[) . x = diff (
u,
x)
by A1, A39, A33, FDIFF_1:def 7;
A42:
((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) . x =
((AffineMap (0,1)) . x) - (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . x)
by A33, A35, A39, VALUED_1:13
.=
((AffineMap (0,1)) . x) - (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) . x) * (sin . x))
by VALUED_1:5
.=
((AffineMap (0,1)) . x) - (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) . x) * (sin . x)) * (sin . x))
by VALUED_1:5
.=
((AffineMap (0,1)) . x) - ((((diff (u,x)) * (diff (u,x))) * (sin . x)) * (sin . x))
by A41, VALUED_1:5
.=
((AffineMap (0,1)) . x) - (((diff (u,x)) ^2) * ((sin . x) ^2))
;
thus ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[) . t =
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) . x
by A33, A39, FUNCT_1:49
.=
(((AffineMap (0,1)) . x) - (((diff (u,x)) ^2) * ((sin . x) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),x))
by AA, A1, A33, A39, Lm19
.=
(((AffineMap (0,1)) . x) - (((diff (u,x)) ^2) * ((sin . x) ^2))) - (((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[) . x)
by A18, A39, A33, FDIFF_1:def 7
.=
(((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) - ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)) . t
by A33, A38, A39, A42, VALUED_1:13
;
verum end;
then A43: integral (((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[),(1 / (n + 1)),(PI - (1 / (n + 1)))) =
integral ((((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) - ((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[)),(1 / (n + 1)),(PI - (1 / (n + 1))))
by A7, B32, A38, RELAT_1:62, FUNCT_1:2
.=
(integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1))))) - (integral (((((u (#) u) (#) sin) (#) cos) `| ].0,PI.[),(1 / (n + 1)),(PI - (1 / (n + 1)))))
by A3, A4, A5, A29, A30, A35, A37, INTEGRA6:12
.=
((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))
by A31
;
integral (((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[),(1 / (n + 1)),(PI - (1 / (n + 1)))) =
integral (((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ].0,PI.[),['(1 / (n + 1)),(PI - (1 / (n + 1)))'])
by INTEGRA5:def 4, A3
.=
integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),['(1 / (n + 1)),(PI - (1 / (n + 1)))'])
by A5, Lm3, RELAT_1:74
.=
integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(1 / (n + 1)),(PI - (1 / (n + 1))))
by A3, INTEGRA5:def 4
;
hence
integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) = ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))
by A43; verum