let y, u be PartFunc of REAL,REAL; 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 = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
let Z be open Subset of REAL; ( 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 = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t)) )
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)) ) )
; for t being Real st t in ].0,PI.[ holds
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
set I = AffineMap (0,1);
set f = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z));
let t be Real; ( t in ].0,PI.[ implies (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t)) )
assume A3:
t in ].0,PI.[
; (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
then
u is_differentiable_in t
by A2, FDIFF_1:9;
then A5:
( u (#) u is_differentiable_in t & diff ((u (#) u),t) = ((u . t) * (diff (u,t))) + ((u . t) * (diff (u,t))) )
by FDIFF_1:16;
A6:
( sin is_differentiable_in t & diff (sin,t) = cos . t )
by SIN_COS:64;
then A7:
( (u (#) u) (#) sin is_differentiable_in t & diff (((u (#) u) (#) sin),t) = ((sin . t) * (diff ((u (#) u),t))) + (((u (#) u) . t) * (diff (sin,t))) )
by A5, FDIFF_1:16;
diff (((u (#) u) (#) sin),t) =
((sin . t) * (((u . t) * (diff (u,t))) + ((u . t) * (diff (u,t))))) + (((u (#) u) . t) * (diff (sin,t)))
by A5, A6, FDIFF_1:16
.=
((((sin . t) * 2) * (u . t)) * (diff (u,t))) + (((u (#) u) . t) * (cos . t))
by SIN_COS:64
;
then (((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t) =
((diff (((u (#) u) (#) sin),t)) * (cos . t)) - (((u (#) u) . t) * ((cos . t) ^2))
.=
((diff (((u (#) u) (#) sin),t)) * (cos . t)) - (((u . t) ^2) * ((cos . t) ^2))
by VALUED_1:5
;
then A8: (((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t =
(((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - (((diff (((u (#) u) (#) sin),t)) * (cos . t)) - (((u . t) ^2) * ((cos . t) ^2)))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1
by A2, A3, Lm18
.=
(((((u . t) ^2) * ((sin . t) ^2)) - ((diff (((u (#) u) (#) sin),t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1
;
( cos is_differentiable_in t & diff (cos,t) = - (sin . t) )
by SIN_COS:63;
then
diff ((((u (#) u) (#) sin) (#) cos),t) = ((cos . t) * (diff (((u (#) u) (#) sin),t))) + ((((u (#) u) (#) sin) . t) * (- (sin . t)))
by A7, FDIFF_1:16;
then - ((diff (((u (#) u) (#) sin),t)) * (cos . t)) =
(- ((((u (#) u) (#) sin) . t) * (sin . t))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
.=
(- ((((u (#) u) . t) * (sin . t)) * (sin . t))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
by VALUED_1:5
.=
(- ((((u . t) * (u . t)) * (sin . t)) * (sin . t))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
by VALUED_1:5
.=
(- (((u . t) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
;
hence
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t))
by A8; verum