let x, y be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) )
let Z be open Subset of REAL; :: thesis: ( x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 implies ( integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) ) )
set I = AffineMap (0,1);
assume A1: ( x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 ) ; :: thesis: ( integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) )
then consider u being PartFunc of REAL,REAL, G being Real_Sequence such that
A2: ( 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)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI ) by Lm23;
A4: ['0,PI'] = [.0,PI.] by LEIBNIZ1:17, INTEGRA5:def 3;
B5: ].0,PI.[ c= [.0,PI.] by Lm1;
then A5: ].0,PI.[ c= Z by A1, A4;
A6: y is_differentiable_on Z by A1, FDIFF_1:26;
then A7: y is_differentiable_on ].0,PI.[ by A5, FDIFF_1:26;
A8: x is_differentiable_on Z by A1, FDIFF_1:26;
then A9: dom (x `| Z) = Z by FDIFF_1:def 7;
A10: y | (dom y) is continuous by A1, FDIFF_1:25;
thus integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI by A2, XXREAL_0:2; :: thesis: ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) )
assume A11: integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI ; :: thesis: ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) )
then for t being Real st t in ].0,PI.[ holds
(u `| ].0,PI.[) . t = 0 by A1, A2, Lm24, Lm26;
then consider C being Real such that
A12: for t being Real st t in ['0,PI'] holds
u . t = C by A2, Th19, LEIBNIZ1:17;

A13: now :: thesis: for t being Real st t in ['0,PI'] holds
y . t = C * (sin . t)

let t be Real; :: thesis: ( t in ['0,PI'] implies y . t = C * (sin . t) )
assume A14: t in ['0,PI'] ; :: thesis: y . t = C * (sin . t)
hence y . t = (y | ['0,PI']) . t by FUNCT_1:49
.= (u (#) sin) . t by A2, A14, FUNCT_1:49
.= (u . t) * (sin . t) by VALUED_1:5
.= C * (sin . t) by A12, A14 ;
:: thesis: verum

end;

A16: integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI)) by A2, A11, XXREAL_0:1;
A18: dom (y (#) (x `| Z)) = (dom y) /\ (dom (x `| Z)) by VALUED_1:def 4
.= (dom y) /\ Z by A8, FDIFF_1:def 7
.= Z by A1, XBOOLE_1:28 ;
(y (#) (x `| Z)) | ['0,PI'] is continuous by A1, A10;
then A20: ( (y (#) (x `| Z)) | ['0,PI'] is bounded & y (#) (x `| Z) is_integrable_on ['0,PI'] ) by A1, A18, INTEGRA5:10, INTEGRA5:11;
set YYXX = (y (#) y) + ((x `| Z) (#) (x `| Z));
A23: dom ((y (#) y) + ((x `| Z) (#) (x `| Z))) = (dom (y (#) y)) /\ (dom ((x `| Z) (#) (x `| Z))) by VALUED_1:def 1
.= ((dom y) /\ (dom y)) /\ (dom ((x `| Z) (#) (x `| Z))) by VALUED_1:def 4
.= (dom y) /\ (Z /\ Z) by A9, VALUED_1:def 4
.= Z by A1, XBOOLE_1:28 ;
((y (#) y) + ((x `| Z) (#) (x `| Z))) | ['0,PI'] is continuous by A1, A10;
then A25: ( ((y (#) y) + ((x `| Z) (#) (x `| Z))) | ['0,PI'] is bounded & (y (#) y) + ((x `| Z) (#) (x `| Z)) is_integrable_on ['0,PI'] ) by A1, A23, INTEGRA5:10, INTEGRA5:11;
A27: ['0,PI'] c= dom ((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) by A1, A23, VALUED_1:def 5;
((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) | ['0,PI'] is continuous by A1, A10;
then A28: ( ((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) | ['0,PI'] is bounded & (1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z))) is_integrable_on ['0,PI'] ) by A27, INTEGRA5:10, INTEGRA5:11;
set J = ((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z));
A30: [.0,PI.] = ['0,PI'] by INTEGRA5:def 3, LEIBNIZ1:17;
A31: dom (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) = (dom ((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z))))) /\ (dom (y (#) (x `| Z))) by VALUED_1:12
.= Z /\ Z by A18, A23, VALUED_1:def 5
.= Z ;
A32: (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) | ['0,PI'] is continuous by A1, A10;
integral (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))),0,PI) = (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI)) by A1, A23, A25, INTEGRA6:10, LEIBNIZ1:17;
then A33: (integral (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))),0,PI)) - (integral ((y (#) (x `| Z)),0,PI)) = 0 by A16;
A34: for t being Real st t in [.0,PI.] holds
0 <= (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t

proof

let t be Real; :: thesis: ( t in [.0,PI.] implies 0 <= (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t )
assume A35: t in [.0,PI.] ; :: thesis: 0 <= (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t
then (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t = (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) . t) - ((y (#) (x `| Z)) . t) by A1, A30, A31, VALUED_1:13
.= ((1 / 2) * (((y (#) y) + ((x `| Z) (#) (x `| Z))) . t)) - ((y (#) (x `| Z)) . t) by VALUED_1:6
.= ((1 / 2) * (((y (#) y) . t) + (((x `| Z) (#) (x `| Z)) . t))) - ((y (#) (x `| Z)) . t) by A1, A23, A30, A35, VALUED_1:def 1 ;
hence 0 <= (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t by Lm7, XREAL_1:48; :: thesis: verum

end;

A40: for t being Real st t in ].0,PI.[ holds
(((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t = 0

proof

assume ex t being Real st
( t in ].0,PI.[ & not (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t = 0 ) ; :: thesis: contradiction
then consider t0 being Real such that
A37: ( t0 in ].0,PI.[ & 0 <> (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t0 ) ;
].0,PI.[ c= [.0,PI.] by Lm1;
then A38: 0 < (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t0 by A34, A37;
[.0,PI.] = ['0,PI'] by INTEGRA5:def 3, LEIBNIZ1:17;
then consider d, c, e being Real such that
A39: ( 0 < e & c < d & c in [.0,PI.] & d in [.0,PI.] & 0 < e * (d - c) & e * (d - c) <= integral ((((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))),0,PI) ) by A1, A31, A32, A34, A37, A38, Th6, LEIBNIZ1:17;
thus contradiction by A1, A18, A20, A27, A28, A33, A39, INTEGRA6:12, LEIBNIZ1:17; :: thesis: verum

end;

A41: for t being Real st t in [.0,PI.] holds
( diff (x,t) = y . t & y . t = C * (sin . t) )

proof

let t be Real; :: thesis: ( t in [.0,PI.] implies ( diff (x,t) = y . t & y . t = C * (sin . t) ) )
assume A42: t in [.0,PI.] ; :: thesis: ( diff (x,t) = y . t & y . t = C * (sin . t) )
then 0 = (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) - (y (#) (x `| Z))) . t by A1, A10, A30, A31, A40, Th1, LEIBNIZ1:17
.= (((1 / 2) (#) ((y (#) y) + ((x `| Z) (#) (x `| Z)))) . t) - ((y (#) (x `| Z)) . t) by A1, A30, A31, A42, VALUED_1:13
.= ((1 / 2) * (((y (#) y) + ((x `| Z) (#) (x `| Z))) . t)) - ((y (#) (x `| Z)) . t) by VALUED_1:6
.= ((1 / 2) * (((y (#) y) . t) + (((x `| Z) (#) (x `| Z)) . t))) - ((y (#) (x `| Z)) . t) by A1, A23, A30, A42, VALUED_1:def 1 ;
then 0 * 2 = (((1 / 2) * (((y (#) y) . t) + (((x `| Z) (#) (x `| Z)) . t))) * 2) - (2 * ((y (#) (x `| Z)) . t))
.= (((y . t) * (y . t)) + (((x `| Z) (#) (x `| Z)) . t)) - (2 * ((y (#) (x `| Z)) . t)) by VALUED_1:5
.= (((y . t) * (y . t)) + (((x `| Z) . t) * ((x `| Z) . t))) - (2 * ((y (#) (x `| Z)) . t)) by VALUED_1:5
.= (((y . t) * (y . t)) + (((x `| Z) . t) * ((x `| Z) . t))) - (2 * ((y . t) * ((x `| Z) . t))) by VALUED_1:5
.= ((y . t) - ((x `| Z) . t)) ^2
.= ((y . t) - (diff (x,t))) ^2 by A1, A8, A30, A42, FDIFF_1:def 7 ;
then 0 = (y . t) - (diff (x,t)) ;
hence diff (x,t) = y . t ; :: thesis: y . t = C * (sin . t)
thus y . t = C * (sin . t) by A13, A30, A42; :: thesis: verum

end;

[.0,PI.] c= dom y by A1, A4;
then A47: dom (y | [.0,PI.]) = [.0,PI.] by RELAT_1:62;
dom (C (#) sin) = REAL by FUNCT_2:def 1;
then A48: dom ((C (#) sin) | [.0,PI.]) = [.0,PI.] by RELAT_1:62;

A50: now :: thesis: for s being object st s in dom (y | [.0,PI.]) holds
(y | [.0,PI.]) . s = ((C (#) sin) | [.0,PI.]) . s

let s be object ; :: thesis: ( s in dom (y | [.0,PI.]) implies (y | [.0,PI.]) . s = ((C (#) sin) | [.0,PI.]) . s )
assume A49: s in dom (y | [.0,PI.]) ; :: thesis: (y | [.0,PI.]) . s = ((C (#) sin) | [.0,PI.]) . s
then reconsider t = s as Real ;
thus (y | [.0,PI.]) . s = y . t by A47, A49, FUNCT_1:49
.= C * (sin . t) by A41, A47, A49
.= (C (#) sin) . s by VALUED_1:6
.= ((C (#) sin) | [.0,PI.]) . s by A47, A49, FUNCT_1:49 ; :: thesis: verum

end;

A52: y | ].0,PI.[ = (y | [.0,PI.]) | ].0,PI.[ by Lm1, RELAT_1:74
.= ((C (#) sin) | [.0,PI.]) | ].0,PI.[ by A47, A48, A50, FUNCT_1:2
.= (C (#) sin) | ].0,PI.[ by Lm1, RELAT_1:74 ;
A54: ].0,PI.[ c= [.0,PI.] by Lm1;
( 0 < PI / 2 & PI / 2 < PI ) by LEIBNIZ1:17, XREAL_1:216;
then A55: PI / 2 in ].0,PI.[ ;
A58: ((y | ].0,PI.[) `| ].0,PI.[) . (PI / 2) = (y `| ].0,PI.[) . (PI / 2) by A5, A6, FDIFF_1:26, Th17
.= diff (y,(PI / 2)) by A7, A55, FDIFF_1:def 7
.= (y `| Z) . (PI / 2) by A5, A6, A55, FDIFF_1:def 7 ;
A59: dom (C (#) sin) = REAL by FUNCT_2:def 1;
A60: sin is_differentiable_on ].0,PI.[ by FDIFF_1:26, SIN_COS:68;
A62: (((C (#) sin) | ].0,PI.[) `| ].0,PI.[) . (PI / 2) = ((C (#) sin) `| ].0,PI.[) . (PI / 2) by Th17, A59, A60, FDIFF_1:20
.= C * (diff (sin,(PI / 2))) by A55, A59, A60, FDIFF_1:20
.= C * (cos . (PI / 2)) by SIN_COS:64 ;
A64: ( diff (x,(PI / 2)) = y . (PI / 2) & y . (PI / 2) = C * (sin . (PI / 2)) ) by A41, A54, A55;
(x `| Z) . (PI / 2) = C * (sin . (PI / 2)) by A5, A8, A55, A64, FDIFF_1:def 7;
then 1 = ((C * (sin . (PI / 2))) ^2) + ((C * (cos . (PI / 2))) ^2) by A1, A4, B5, A52, A55, A58, A62
.= (C ^2) * (((sin . (PI / 2)) ^2) + ((cos . (PI / 2)) ^2))
.= (C ^2) * 1 by SIN_COS:28
.= C ^2 ;
then A65: 1 ^2 = C ^2 ;
A66: [.0,PI.] c= Z by A1, LEIBNIZ1:17, INTEGRA5:def 3;
then [.0,PI.] c= dom (x `| Z) by A8, FDIFF_1:def 7;
then A67: dom ((x `| Z) | [.0,PI.]) = [.0,PI.] by RELAT_1:62;

A68: now :: thesis: for s being object st s in dom ((x `| Z) | [.0,PI.]) holds
((x `| Z) | [.0,PI.]) . s = (y | [.0,PI.]) . s

let s be object ; :: thesis: ( s in dom ((x `| Z) | [.0,PI.]) implies ((x `| Z) | [.0,PI.]) . s = (y | [.0,PI.]) . s )
assume A69: s in dom ((x `| Z) | [.0,PI.]) ; :: thesis: ((x `| Z) | [.0,PI.]) . s = (y | [.0,PI.]) . s
then reconsider t = s as Real ;
thus ((x `| Z) | [.0,PI.]) . s = (x `| Z) . s by A67, A69, FUNCT_1:49
.= diff (x,t) by A8, A66, A67, A69, FDIFF_1:def 7
.= y . t by A41, A67, A69
.= (y | [.0,PI.]) . s by A67, A69, FUNCT_1:49 ; :: thesis: verum

end;

A71: x is_differentiable_on Z by A1, FDIFF_1:26;
x `| Z = (x `| Z) | Z by A9;
then A72: x is_integral_of x `| Z,Z by A71, INTEGRA7:def 1;

A73: now :: thesis: for t being Real st t in [.0,PI.] holds
( diff (x,t) = y . t & y . t = C * (sin . t) & x . t = ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0) )

let t be Real; :: thesis: ( t in [.0,PI.] implies ( diff (x,t) = y . t & y . t = C * (sin . t) & x . t = ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0) ) )
assume A74: t in [.0,PI.] ; :: thesis: ( diff (x,t) = y . t & y . t = C * (sin . t) & x . t = ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0) )
hence ( diff (x,t) = y . t & y . t = C * (sin . t) ) by A41; :: thesis: x . t = ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0)
A75: ( 0 <= t & t <= PI ) by A74, XXREAL_1:1;
A77: [.0,t.] c= Z

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in [.0,t.] or s in Z )
assume B75: s in [.0,t.] ; :: thesis: s in Z
reconsider g = s as Real by B75;
( 0 <= g & g <= t ) by B75, XXREAL_1:1;
then ( 0 <= g & g <= PI ) by A75, XXREAL_0:2;
then g in [.0,PI.] ;
hence s in Z by A1, A4; :: thesis: verum

end;

A78: (x `| Z) | Z is continuous by A1;
A79: dom sin = REAL by FUNCT_2:def 1;
sin | ['0,t'] is continuous ;
then A80: ( sin | ['0,t'] is bounded & sin is_integrable_on ['0,t'] ) by A79, INTEGRA5:10, INTEGRA5:11;
A82: ['0,t'] c= [.0,PI.]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ['0,t'] or z in [.0,PI.] )
assume A81: z in ['0,t'] ; :: thesis: z in [.0,PI.]
then reconsider s = z as Real ;
s in [.0,t.] by A75, A81, INTEGRA5:def 3;
then ( 0 <= s & s <= t ) by XXREAL_1:1;
then ( 0 <= s & s <= PI ) by A75, XXREAL_0:2;
hence z in [.0,PI.] ; :: thesis: verum

end;

A83: y || ['0,t'] = (y | [.0,PI.]) | ['0,t'] by A82, RELAT_1:74
.= ((C (#) sin) | [.0,PI.]) | ['0,t'] by A47, A48, A50, FUNCT_1:2
.= (C (#) sin) || ['0,t'] by A82, RELAT_1:74 ;
A84: y || ['0,t'] = (y | [.0,PI.]) | ['0,t'] by A82, RELAT_1:74
.= ((x `| Z) | [.0,PI.]) | ['0,t'] by A47, A67, A68, FUNCT_1:2
.= (x `| Z) || ['0,t'] by A82, RELAT_1:74 ;
thus x . t = (integral ((x `| Z),0,t)) + (x . 0) by A9, A72, A75, A77, A78, INTEGRA7:20
.= (integral ((x `| Z),['0,t'])) + (x . 0) by A75, INTEGRA5:def 4
.= (integral ((C (#) sin),['0,t'])) + (x . 0) by A83, A84
.= (integral ((C (#) sin),0,t)) + (x . 0) by A75, INTEGRA5:def 4
.= (C * (integral (sin,0,t))) + (x . 0) by A75, A79, A80, INTEGRA6:10
.= (C * ((cos . 0) - (cos . t))) + (x . 0) by INTEGRA7:26
.= ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0) ; :: thesis: verum

end;

thus ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) :: thesis: verum

proof

per cases ( C = 1 or C = - 1 ) by A65, SQUARE_1:40;

suppose A85: C = 1 ; :: thesis: ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) )

for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) )

proof

let t be Real; :: thesis: ( t in [.0,PI.] implies ( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) )
assume A86: t in [.0,PI.] ; :: thesis: ( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) )
then A87: ( diff (x,t) = y . t & y . t = C * (sin . t) ) by A73;
x . t = ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0) by A73, A86;
hence ( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) by A85, A87; :: thesis: verum

end;

hence ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) ; :: thesis: verum

end;

suppose A89: C = - 1 ; :: thesis: ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) )

for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) )

proof

let t be Real; :: thesis: ( t in [.0,PI.] implies ( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) )
assume A90: t in [.0,PI.] ; :: thesis: ( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) )
then A91: ( diff (x,t) = y . t & y . t = C * (sin . t) ) by A73;
x . t = ((- (C * (cos . t))) + (C * (cos . 0))) + (x . 0) by A73, A90;
hence ( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) by A89, A91; :: thesis: verum

end;

hence ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) ; :: thesis: verum

end;

end;

end;