theorem :: CURVE:5

for a, b, l being Real
for x, y being PartFunc of REAL,REAL st a < b & (ArcLenP (x,y,a,b)) . b = l & y . a = 0 & y . b = 0 & x is differentiable & y is differentiable & [.a,b.] c= dom x & [.a,b.] 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
0 < ((diff (x,t)) ^2) + ((diff (y,t)) ^2) ) holds
( integral ((y (#) (x `| (dom x))),a,b) <= ((1 / 2) * (l ^2)) / PI & ( not integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI or for s being Real st s in [.a,b.] holds
( y . s = (l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) & x . s = (l / PI) * (((- (cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) + (cos . 0)) + ((PI / l) * (x . a))) ) or for s being Real st s in [.a,b.] holds
( y . s = - ((l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) & x . s = (l / PI) * (((cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) - (cos . 0)) + ((PI / l) * (x . a))) ) ) & ( ( for s being Real st s in [.a,b.] holds
( y . s = (l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) & x . s = (l / PI) * (((- (cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) + (cos . 0)) + ((PI / l) * (x . a))) ) or for s being Real st s in [.a,b.] holds
( y . s = - ((l / PI) * (sin . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l))) & x . s = (l / PI) * (((cos . ((PI * ((ArcLenP (x,y,a,b)) . s)) / l)) - (cos . 0)) + ((PI / l) * (x . a))) ) ) implies integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI ) )