let y, u be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL st y is differentiable & ['0,PI'] c= Z & Z c= dom y & 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 t being Real st t in ].0,PI.[ holds
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1
let Z be open Subset of REAL; :: thesis: ( y is differentiable & ['0,PI'] c= Z & Z c= dom y & 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 t being Real st t in ].0,PI.[ holds
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1 )
assume A2: ( y is differentiable & ['0,PI'] c= Z & Z c= dom y & 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: for t being Real st t in ].0,PI.[ holds
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1
['0,PI'] = [.0,PI.] by INTEGRA5:def 3, LmPI;
then A3: ].0,PI.[ c= ['0,PI'] by Lm1;
set I = AffineMap (0,1);
A1: dom (AffineMap (0,1)) = REAL by FUNCT_2:def 1;
A5: y is_differentiable_on Z by A2, FDIFF_1:26;
set f = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z));
set g = ((((u (#) u) (#) ((sin (#) sin) - (cos (#) cos))) - ((((2 (#) u) (#) (u `| ].0,PI.[)) (#) sin) (#) cos)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)) + (AffineMap (0,1));
set Z0 = ].0,PI.[;
dom (y (#) y) = (dom y) /\ (dom y) by VALUED_1:def 4
.= dom y ;
then A7: dom ((y (#) y) + (AffineMap (0,1))) = (dom y) /\ REAL by A1, VALUED_1:def 1
.= dom y by XBOOLE_1:28 ;
dom ((y `| Z) (#) (y `| Z)) = (dom (y `| Z)) /\ (dom (y `| Z)) by VALUED_1:def 4
.= Z by A5, FDIFF_1:def 7 ;
then A8: dom (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) = Z /\ (dom y) by VALUED_1:12, A7
.= Z by A2, XBOOLE_1:28 ;
let t be Real; :: thesis: ( t in ].0,PI.[ implies (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1 )
assume A9: t in ].0,PI.[ ; :: thesis: (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1
then A10: t in Z by A2;
AA: (AffineMap (0,1)) . t = (0 * t) + 1 by FCONT_1:def 4;
A12: y . t = (y | ['0,PI']) . t by A3, A9, FUNCT_1:49
.= (u (#) sin) . t by A2, A9, FUNCT_1:49
.= (u . t) * (sin . t) by VALUED_1:5 ;
A13: t in dom ((y (#) y) + (AffineMap (0,1))) by A2, A7, A9;
thus (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((y (#) y) + (AffineMap (0,1))) . t) - (((y `| Z) (#) (y `| Z)) . t) by A2, A8, A9, VALUED_1:13
.= (((y (#) y) . t) + ((AffineMap (0,1)) . t)) - (((y `| Z) (#) (y `| Z)) . t) by A13, VALUED_1:def 1
.= (((y . t) * (y . t)) + ((AffineMap (0,1)) . t)) - (((y `| Z) (#) (y `| Z)) . t) by VALUED_1:5
.= (((y . t) * (y . t)) + ((AffineMap (0,1)) . t)) - (((y `| Z) . t) * ((y `| Z) . t)) by VALUED_1:5
.= (((y . t) * (y . t)) + ((AffineMap (0,1)) . t)) - ((diff (y,t)) * ((y `| Z) . t)) by A5, A10, FDIFF_1:def 7
.= ((((u . t) ^2) * ((sin . t) ^2)) + 1) - ((diff (y,t)) * (diff (y,t))) by A5, A10, A12, FDIFF_1:def 7, AA
.= ((((u . t) ^2) * ((sin . t) ^2)) + 1) - ((((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t))) * (diff (y,t))) by A2, A9
.= ((((u . t) ^2) * ((sin . t) ^2)) + 1) - ((((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t))) * (((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)))) by A2, A9
.= (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1 ; :: thesis: verum