let y, u be PartFunc of REAL,REAL; :: thesis: 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
ex F being Real_Sequence st
( ( for n being Nat holds F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & F is convergent & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) = lim F )
let Z0 be open Subset of REAL; :: thesis: ( 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 ex F being Real_Sequence st
( ( for n being Nat holds F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & F is convergent & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) = lim F ) )
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)) ) ) ; :: thesis: ex F being Real_Sequence st
( ( for n being Nat holds F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & F is convergent & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) = lim F )
set I = AffineMap (0,1);
A4: ['0,PI'] = [.0,PI.] by INTEGRA5:def 3, LmPI;
y is_differentiable_on Z0 by A1, FDIFF_1:26;
then A5: dom (y `| Z0) = Z0 by FDIFF_1:def 7;
set G = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0));
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 A6: 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 A5, VALUED_1:def 4
.= Z0 ;
then B6: dom (((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) = (dom y) /\ Z0 by A6, VALUED_1:12
.= Z0 by A1, XBOOLE_1:28 ;
y | (dom y) is continuous by A1, FDIFF_1:25;
then (((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))) | ['0,PI'] is continuous by A1;
then consider S1 being Real_Sequence such that
A9: ( ( for n being Nat holds S1 . n = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) ) & S1 is convergent & lim S1 = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) ) by A1, B6, Th7, LmPI;
deffunc H1( Nat) -> Element of REAL = In ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / ($1 + 1)),(PI - (1 / ($1 + 1))))),REAL);
consider S2 being Function of NAT,REAL such that
A10: for x being Element of NAT holds S2 . x = H1(x) from FUNCT_2:sch 4();
 A11: for n being Nat holds S2 . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1))))
proof
let n be Nat; :: thesis: S2 . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1))))
n in NAT by ORDINAL1:def 12;
hence S2 . n = In ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1))))),REAL) by A10
.= integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ;
:: thesis: verum
end;
deffunc H2( Nat) -> Element of REAL = In ((1 / ($1 + 1)),REAL);
consider S32 being Function of NAT,REAL such that
A12: for x being Element of NAT holds S32 . x = H2(x) from FUNCT_2:sch 4();
 A13: for n being Nat holds S32 . n = 1 / (n + 1)
proof
let n be Nat; :: thesis: S32 . n = 1 / (n + 1)
n in NAT by ORDINAL1:def 12;
hence S32 . n = In ((1 / (n + 1)),REAL) by A12
.= 1 / (n + 1) ;
:: thesis: verum
end;
then A14: ( S32 is convergent & lim S32 = 0 ) by SEQ_4:31;
consider S310 being constant Function of NAT,REAL such that
A16: for x being Nat holds S310 . x = PI by LmX;
S310 . 0 = PI by A16;
then A19: ( S310 is convergent & lim S310 = PI ) by SEQ_4:25;
set S31 = S310 - S32;
A20: ((u (#) u) (#) sin) (#) cos is continuous by A1;
A21: ( S310 - S32 is convergent & lim (S310 - S32) = (lim S310) - (lim S32) ) by A14, SEQ_2:12;
A23: for n being Nat holds (S310 - S32) . n = PI - (1 / (n + 1))
proof
let n be Nat; :: thesis: (S310 - S32) . n = PI - (1 / (n + 1))
thus (S310 - S32) . n = (S310 . n) + ((- S32) . n) by SEQ_1:7
.= (S310 . n) + (- (S32 . n)) by SEQ_1:10
.= PI - (S32 . n) by A16
.= PI - (1 / (n + 1)) by A13 ; :: thesis: verum
end;
A24: ( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;
set UUSC = ((u (#) u) (#) sin) (#) cos;
A25: dom (((u (#) u) (#) sin) (#) cos) = (dom ((u (#) u) (#) sin)) /\ REAL by A24, VALUED_1:def 4
.= ((dom (u (#) u)) /\ REAL) /\ REAL by A24, VALUED_1:def 4
.= (([.0,PI.] /\ [.0,PI.]) /\ REAL) /\ REAL by A1, A4, VALUED_1:def 4
.= [.0,PI.] /\ (REAL /\ REAL) by XBOOLE_1:16
.= [.0,PI.] by XBOOLE_1:28 ;
then PI in dom (((u (#) u) (#) sin) (#) cos) by LmPI;
then A26: ((u (#) u) (#) sin) (#) cos is_continuous_in PI by A20;
A30: rng (S310 - S32) c= dom (((u (#) u) (#) sin) (#) cos)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (S310 - S32) or y in dom (((u (#) u) (#) sin) (#) cos) )
assume y in rng (S310 - S32) ; :: thesis: y in dom (((u (#) u) (#) sin) (#) cos)
then consider n being object such that
A27: ( n in dom (S310 - S32) & y = (S310 - S32) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A27;
A28: y = PI - (1 / (n + 1)) by A23, A27;
A29: 0 < PI - (1 / (n + 1)) by Lm3;
PI - (1 / (n + 1)) < PI by Lm3;
hence y in dom (((u (#) u) (#) sin) (#) cos) by A25, A28, A29; :: thesis: verum
end;
then A31: ( (((u (#) u) (#) sin) (#) cos) /* (S310 - S32) is convergent & (((u (#) u) (#) sin) (#) cos) . PI = lim ((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) ) by A14, A19, A21, A26;
A32: lim ((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) = (((u (#) u) (#) sin) . PI) * (cos . PI) by A31, VALUED_1:5
.= (((u (#) u) . PI) * (sin . PI)) * (cos . PI) by VALUED_1:5
.= 0 by SIN_COS:77 ;
0 in dom (((u (#) u) (#) sin) (#) cos) by A25, LEIBNIZ1:17;
then A33: ((u (#) u) (#) sin) (#) cos is_continuous_in 0 by A20;
A36: rng S32 c= dom (((u (#) u) (#) sin) (#) cos)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng S32 or y in dom (((u (#) u) (#) sin) (#) cos) )
assume y in rng S32 ; :: thesis: y in dom (((u (#) u) (#) sin) (#) cos)
then consider n being object such that
A34: ( n in dom S32 & y = S32 . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A34;
A35: y = 1 / (n + 1) by A13, A34;
( 1 / (n + 1) < PI - (1 / (n + 1)) & PI - (1 / (n + 1)) < PI ) by Lm3;
then 1 / (n + 1) < PI by XXREAL_0:2;
hence y in dom (((u (#) u) (#) sin) (#) cos) by A25, A35; :: thesis: verum
end;
then A37: ( (((u (#) u) (#) sin) (#) cos) /* S32 is convergent & (((u (#) u) (#) sin) (#) cos) . 0 = lim ((((u (#) u) (#) sin) (#) cos) /* S32) ) by A14, A33;
A38: lim ((((u (#) u) (#) sin) (#) cos) /* S32) = (((u (#) u) (#) sin) . 0) * (cos . 0) by A37, VALUED_1:5
.= (((u (#) u) . 0) * (sin . 0)) * (cos . 0) by VALUED_1:5
.= 0 by SIN_COS:30 ;
set S3 = ((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32);
A40: lim (((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) = 0 - 0 by A31, A32, A37, A38, SEQ_2:12
.= 0 ;
now :: thesis: for n being Nat holds S2 . n = (S1 . n) + ((((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) . n)
let n be Nat; :: thesis: S2 . n = (S1 . n) + ((((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) . n)
A41: n is Element of NAT by ORDINAL1:def 12;
A42: (((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) . n = (((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) . n) + ((- ((((u (#) u) (#) sin) (#) cos) /* S32)) . n) by SEQ_1:7
.= (((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) . n) + (- (((((u (#) u) (#) sin) (#) cos) /* S32) . n)) by SEQ_1:10
.= ((((u (#) u) (#) sin) (#) cos) . ((S310 - S32) . n)) - (((((u (#) u) (#) sin) (#) cos) /* S32) . n) by A30, A41, FUNCT_2:108
.= ((((u (#) u) (#) sin) (#) cos) . ((S310 - S32) . n)) - ((((u (#) u) (#) sin) (#) cos) . (S32 . n)) by A36, A41, FUNCT_2:108
.= ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1)))) - ((((u (#) u) (#) sin) (#) cos) . (S32 . n)) by A23
.= ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1)))) - ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1))) by A13 ;
S1 . n = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) by A9
.= ((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 A1, Lm20
.= ((S2 . n) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1))) by A11
.= (S2 . n) - ((((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) . n) by A42 ;
hence S2 . n = (S1 . n) + ((((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) . n) ; :: thesis: verum
end;
then A43: S2 = S1 + (((((u (#) u) (#) sin) (#) cos) /* (S310 - S32)) - ((((u (#) u) (#) sin) (#) cos) /* S32)) by SEQ_1:7;
take S2 ; :: thesis: ( ( for n being Nat holds S2 . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & S2 is convergent & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) = lim S2 )
lim S2 = (lim S1) - 0 by A9, A31, A37, A40, A43, SEQ_2:6
.= integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) by A9 ;
hence ( ( for n being Nat holds S2 . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & S2 is convergent & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) = lim S2 ) by A9, A11, A31, A37, A43; :: thesis: verum