let x, y be PartFunc of REAL,REAL; :: thesis: for L being Real st 0 < L & x is differentiable & y is differentiable & [.0,PI.] c= dom x & [.0,PI.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = L / PI ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * L & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L or for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L ) )
let L be Real; :: thesis: ( 0 < L & x is differentiable & y is differentiable & [.0,PI.] c= dom x & [.0,PI.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = L / PI ) & y . 0 = 0 & y . PI = 0 implies ( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * L & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L or for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L ) ) )
assume that
A1: 0 < L and
A2: ( x is differentiable & y is differentiable & [.0,PI.] c= dom x & [.0,PI.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = L / PI ) & y . 0 = 0 & y . PI = 0 ) ; :: thesis: ( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * L & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L or for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L ) )
set k = sqrt (PI / L);
set x1 = (sqrt (PI / L)) (#) x;
set y1 = (sqrt (PI / L)) (#) y;
A5: (sqrt (PI / L)) ^2 = PI / L by A1, LmPI, SQUARE_1:def 2;
A6: ['0,PI'] = [.0,PI.] by INTEGRA5:def 3, LmPI;
A7: ( dom ((sqrt (PI / L)) (#) x) = dom x & dom ((sqrt (PI / L)) (#) y) = dom y ) by VALUED_1:def 5;
reconsider Z1 = dom x, Z2 = dom y as open Subset of REAL by A2, FDIFF_1:10;
A8: ( (sqrt (PI / L)) (#) x is_differentiable_on Z1 & ((sqrt (PI / L)) (#) x) `| Z1 = (sqrt (PI / L)) (#) (x `| Z1) & (sqrt (PI / L)) (#) y is_differentiable_on Z2 & ((sqrt (PI / L)) (#) y) `| Z2 = (sqrt (PI / L)) (#) (y `| Z2) ) by A2, A7, Th12;
A10: for t being Real st t in (dom ((sqrt (PI / L)) (#) x)) /\ (dom ((sqrt (PI / L)) (#) y)) holds
((diff (((sqrt (PI / L)) (#) x),t)) ^2) + ((diff (((sqrt (PI / L)) (#) y),t)) ^2) = 1

proof

let t be Real; :: thesis: ( t in (dom ((sqrt (PI / L)) (#) x)) /\ (dom ((sqrt (PI / L)) (#) y)) implies ((diff (((sqrt (PI / L)) (#) x),t)) ^2) + ((diff (((sqrt (PI / L)) (#) y),t)) ^2) = 1 )
assume A11: t in (dom ((sqrt (PI / L)) (#) x)) /\ (dom ((sqrt (PI / L)) (#) y)) ; :: thesis: ((diff (((sqrt (PI / L)) (#) x),t)) ^2) + ((diff (((sqrt (PI / L)) (#) y),t)) ^2) = 1
then A12: ((diff (x,t)) ^2) + ((diff (y,t)) ^2) = L / PI by A2, A7;
A13: t in dom ((sqrt (PI / L)) (#) x) by A11, XBOOLE_0:def 4;
then A14: diff (((sqrt (PI / L)) (#) x),t) = (((sqrt (PI / L)) (#) x) `| Z1) . t by A7, A8, FDIFF_1:def 7
.= (sqrt (PI / L)) * ((x `| Z1) . t) by A8, VALUED_1:6
.= (sqrt (PI / L)) * (diff (x,t)) by A2, A7, A13, FDIFF_1:def 7 ;
A15: t in dom ((sqrt (PI / L)) (#) y) by A11, XBOOLE_0:def 4;
then diff (((sqrt (PI / L)) (#) y),t) = (((sqrt (PI / L)) (#) y) `| Z2) . t by A7, A8, FDIFF_1:def 7
.= (sqrt (PI / L)) * ((y `| Z2) . t) by A8, VALUED_1:6
.= (sqrt (PI / L)) * (diff (y,t)) by A2, A7, A15, FDIFF_1:def 7 ;
hence ((diff (((sqrt (PI / L)) (#) x),t)) ^2) + ((diff (((sqrt (PI / L)) (#) y),t)) ^2) = ((sqrt (PI / L)) ^2) * (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) by A14
.= (PI * L) / (PI * L) by A5, A12, XCMPLX_1:76
.= 1 by A1, LmPI, XCMPLX_1:60 ;
:: thesis: verum

end;

A18: ((sqrt (PI / L)) (#) y) . 0 = (sqrt (PI / L)) * (y . 0) by VALUED_1:6
.= 0 by A2 ;
A19: ((sqrt (PI / L)) (#) y) . PI = (sqrt (PI / L)) * (y . PI) by VALUED_1:6
.= 0 by A2 ;
B19: ( (sqrt (PI / L)) (#) x is differentiable & (sqrt (PI / L)) (#) y is differentiable ) by A8, VALUED_1:def 5;
then A20: ( integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) <= (1 / 2) * PI & ( not integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) or for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) or for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) ) implies integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * PI ) ) by A2, A6, A7, A8, A10, A18, A19, Th22;
set g = y (#) (x `| Z1);
A21: ((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| Z1) = (sqrt (PI / L)) (#) (((sqrt (PI / L)) (#) y) (#) (x `| Z1)) by A8, RFUNCT_1:13
.= (sqrt (PI / L)) (#) ((sqrt (PI / L)) (#) (y (#) (x `| Z1))) by RFUNCT_1:12
.= (PI / L) (#) (y (#) (x `| Z1)) by A5, RFUNCT_1:17 ;
A22: dom (y (#) (x `| Z1)) = (dom y) /\ (dom (x `| Z1)) by VALUED_1:def 4
.= (dom x) /\ (dom y) by A2, FDIFF_1:def 7 ;
y is_differentiable_on dom y by A2;
then y is continuous by FDIFF_1:25;
then (y (#) (x `| Z1)) | ['0,PI'] is continuous by A2;
then B22: ( y (#) (x `| Z1) is_integrable_on ['0,PI'] & (y (#) (x `| Z1)) | ['0,PI'] is bounded ) by A2, A6, A22, INTEGRA5:10, INTEGRA5:11, XBOOLE_1:19;
then A23: integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (PI / L) * (integral ((y (#) (x `| (dom x))),0,PI)) by A2, A6, A7, A21, A22, INTEGRA6:10, LmPI, XBOOLE_1:19;
then ((PI / L) * (integral ((y (#) (x `| (dom x))),0,PI))) * L <= ((1 / 2) * PI) * L by A1, A20, XREAL_1:64;
then ((PI / L) * L) * (integral ((y (#) (x `| (dom x))),0,PI)) <= ((1 / 2) * PI) * L ;
then PI * (integral ((y (#) (x `| (dom x))),0,PI)) <= ((1 / 2) * PI) * L by A1, XCMPLX_1:87;
then (PI * (integral ((y (#) (x `| (dom x))),0,PI))) / PI <= (((1 / 2) * PI) * L) / PI by LmPI, XREAL_1:72;
then integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * ((PI * L) / PI) by LmPI, XCMPLX_1:89;
hence integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * L by LmPI, XCMPLX_1:89; :: thesis: ( integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L iff ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) )
A24: ( integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * PI iff integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L )

proof

hereby :: thesis: ( integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L implies integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * PI )

assume integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * PI ; :: thesis: integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L
then ((PI / L) * (integral ((y (#) (x `| (dom x))),0,PI))) * L = ((1 / 2) * PI) * L by A2, A6, A7, A21, A22, B22, INTEGRA6:10, LmPI, XBOOLE_1:19;
then ((PI / L) * L) * (integral ((y (#) (x `| (dom x))),0,PI)) = ((1 / 2) * PI) * L ;
then (PI * (integral ((y (#) (x `| (dom x))),0,PI))) / PI = (((1 / 2) * PI) * L) / PI by A1, XCMPLX_1:87;
hence integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * (PI * (L / PI)) by LmPI, XCMPLX_1:89
.= (1 / 2) * L by LmPI, XCMPLX_1:87 ;
:: thesis: verum

end;

assume integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L ; :: thesis: integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * PI
hence integral ((((sqrt (PI / L)) (#) y) (#) (((sqrt (PI / L)) (#) x) `| (dom ((sqrt (PI / L)) (#) x)))),0,PI) = (1 / 2) * ((PI / L) * L) by A23
.= (1 / 2) * PI by A1, XCMPLX_1:87 ;
:: thesis: verum

end;

A25: sqrt (PI / L) <> 0 by A1, LmPI, SQUARE_1:25;
A26: ( ( for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) ) iff for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) )

proof

hereby :: thesis: ( ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) implies for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) )

assume A27: for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) ; :: thesis: for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) )
let t be Real; :: thesis: ( t in [.0,PI.] implies ( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) )
assume t in [.0,PI.] ; :: thesis: ( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) )
then ( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) by A27;
then ( (sqrt (PI / L)) * (y . t) = sin . t & (sqrt (PI / L)) * (x . t) = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) by VALUED_1:6;
then ( (sqrt (PI / L)) * (y . t) = sin . t & (sqrt (PI / L)) * (x . t) = ((- (cos . t)) + (cos . 0)) + ((sqrt (PI / L)) * (x . 0)) ) by VALUED_1:6;
then A28: ( ((sqrt (PI / L)) * (y . t)) / (sqrt (PI / L)) = (sin . t) / (sqrt (PI / L)) & ((sqrt (PI / L)) * (x . t)) / (sqrt (PI / L)) = ((- (cos . t)) + ((cos . 0) + ((sqrt (PI / L)) * (x . 0)))) / (sqrt (PI / L)) ) ;
((cos . 0) + ((sqrt (PI / L)) * (x . 0))) / (sqrt (PI / L)) = ((cos . 0) / (sqrt (PI / L))) + (((sqrt (PI / L)) * (x . 0)) / (sqrt (PI / L)))
.= ((cos . 0) / (sqrt (PI / L))) + (x . 0) by A25, XCMPLX_1:89 ;
hence ( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) by A25, A28, XCMPLX_1:89; :: thesis: verum

end;

assume A29: for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ; :: thesis: for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) )
let t be Real; :: thesis: ( t in [.0,PI.] implies ( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) )
assume t in [.0,PI.] ; :: thesis: ( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) )
then ( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) by A29;
then A30: ( ((sqrt (PI / L)) (#) y) . t = ((sin . t) / (sqrt (PI / L))) * (sqrt (PI / L)) & ((sqrt (PI / L)) (#) x) . t = (((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0)) * (sqrt (PI / L)) ) by VALUED_1:6;
then ((sqrt (PI / L)) (#) x) . t = ((- (((cos . t) / (sqrt (PI / L))) * (sqrt (PI / L)))) + (((cos . 0) / (sqrt (PI / L))) * (sqrt (PI / L)))) + ((x . 0) * (sqrt (PI / L)))
.= ((- (cos . t)) + (((cos . 0) / (sqrt (PI / L))) * (sqrt (PI / L)))) + ((x . 0) * (sqrt (PI / L))) by A25, XCMPLX_1:87
.= ((- (cos . t)) + (cos . 0)) + ((x . 0) * (sqrt (PI / L))) by A25, XCMPLX_1:87
.= ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) by VALUED_1:6 ;
hence ( ((sqrt (PI / L)) (#) y) . t = sin . t & ((sqrt (PI / L)) (#) x) . t = ((- (cos . t)) + (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) by A25, A30, XCMPLX_1:87; :: thesis: verum

end;

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

proof

hereby :: thesis: ( ( for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) implies for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) )

assume A31: for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) ; :: thesis: for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) )
let t be Real; :: thesis: ( t in [.0,PI.] implies ( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) )
assume t in [.0,PI.] ; :: thesis: ( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) )
then ( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) by A31;
then ( (sqrt (PI / L)) * (y . t) = - (sin . t) & (sqrt (PI / L)) * (x . t) = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) by VALUED_1:6;
then ( (sqrt (PI / L)) * (y . t) = - (sin . t) & (sqrt (PI / L)) * (x . t) = ((cos . t) - (cos . 0)) + ((sqrt (PI / L)) * (x . 0)) ) by VALUED_1:6;
then A32: ( ((sqrt (PI / L)) * (y . t)) / (sqrt (PI / L)) = (- (sin . t)) / (sqrt (PI / L)) & ((sqrt (PI / L)) * (x . t)) / (sqrt (PI / L)) = ((cos . t) + ((- (cos . 0)) + ((sqrt (PI / L)) * (x . 0)))) / (sqrt (PI / L)) ) ;
((- (cos . 0)) + ((sqrt (PI / L)) * (x . 0))) / (sqrt (PI / L)) = (- ((cos . 0) / (sqrt (PI / L)))) + (((sqrt (PI / L)) * (x . 0)) / (sqrt (PI / L)))
.= (- ((cos . 0) / (sqrt (PI / L)))) + (x . 0) by A25, XCMPLX_1:89 ;
hence ( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) by A25, A32, XCMPLX_1:89; :: thesis: verum

end;

assume A33: for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ; :: thesis: for t being Real st t in [.0,PI.] holds
( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) )
let t be Real; :: thesis: ( t in [.0,PI.] implies ( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) )
assume t in [.0,PI.] ; :: thesis: ( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) )
then ( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) by A33;
then B33: ( (y . t) * (sqrt (PI / L)) = (- ((sin . t) / (sqrt (PI / L)))) * (sqrt (PI / L)) & (x . t) * (sqrt (PI / L)) = ((((cos . t) / (sqrt (PI / L))) + (- ((cos . 0) / (sqrt (PI / L))))) + (x . 0)) * (sqrt (PI / L)) ) ;
then A34: ( ((sqrt (PI / L)) (#) y) . t = - (((sin . t) / (sqrt (PI / L))) * (sqrt (PI / L))) & ((sqrt (PI / L)) (#) x) . t = ((((cos . t) / (sqrt (PI / L))) + (- ((cos . 0) / (sqrt (PI / L))))) + (x . 0)) * (sqrt (PI / L)) ) by VALUED_1:6;
((sqrt (PI / L)) (#) x) . t = ((((cos . t) / (sqrt (PI / L))) * (sqrt (PI / L))) - (((cos . 0) / (sqrt (PI / L))) * (sqrt (PI / L)))) + ((x . 0) * (sqrt (PI / L))) by B33, VALUED_1:6
.= ((cos . t) - (((cos . 0) / (sqrt (PI / L))) * (sqrt (PI / L)))) + ((x . 0) * (sqrt (PI / L))) by A25, XCMPLX_1:87
.= ((cos . t) - (cos . 0)) + ((x . 0) * (sqrt (PI / L))) by A25, XCMPLX_1:87
.= ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) by VALUED_1:6 ;
hence ( ((sqrt (PI / L)) (#) y) . t = - (sin . t) & ((sqrt (PI / L)) (#) x) . t = ((cos . t) - (cos . 0)) + (((sqrt (PI / L)) (#) x) . 0) ) by A25, A34, XCMPLX_1:87; :: thesis: verum

end;

hence ( integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L iff ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) ) by A2, A6, A7, A8, A10, A18, A19, B19, A24, A26, Th22; :: thesis: verum