theorem :: PDLAX:17

for x, y being PartFunc of REAL,REAL
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 ) )