let a, b, l be Real; :: thesis:
let x, y be PartFunc of REAL,REAL; :: thesis:
assume A1: ( 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) ) ) ; :: thesis:
then consider a1, b1 being Real, L being one-to-one PartFunc of REAL,REAL such that
A2: ( a1 < a & b < b1 & [.a1,b1.] c= (dom x) /\ (dom y) & dom L = ].a1,b1.[ & ( for t being Real st t in ].a1,b1.[ holds
L . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a1,t) ) & ( for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = (L . t) - (L . a) ) & L is increasing & L | [.a,b.] is continuous & L .: [.a,b.] = [.(L . a),(L . b).] & ( for t being Real st t in ].a1,b1.[ holds
L is_differentiable_in t ) & L is_differentiable_on ].a1,b1.[ & ( for t being Real st t in ].a1,b1.[ holds
diff (L,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) ) & L " is_differentiable_on dom (L ") & ( for t being Real st t in dom (L ") holds
diff ((L "),t) = 1 / (diff (L,((L ") . t))) ) & L " is continuous & ( for s being Real st s in rng L holds
( x * (L ") is_differentiable_in s & y * (L ") is_differentiable_in s & diff ((x * (L ")),s) = (diff (x,((L ") . s))) * (diff ((L "),s)) & diff ((y * (L ")),s) = (diff (y,((L ") . s))) * (diff ((L "),s)) & ((diff ((x * (L ")),s)) ^2) + ((diff ((y * (L ")),s)) ^2) = 1 ) ) & (x * (L ")) `| (dom (x * (L "))) = ((x `| (dom x)) * (L ")) (#) ((L ") `| (dom (L "))) & (y * (L ")) `| (dom (y * (L "))) = ((y `| (dom y)) * (L ")) (#) ((L ") `| (dom (L "))) & (L ") `| (dom (L ")) = ((L `| (dom L)) * (L ")) ^ & (L ") `| (dom (L ")) is continuous & [.(L . a),(L . b).] c= dom (L ") & [.(L . a),(L . b).] c= dom (x * (L ")) & [.(L . a),(L . b).] c= dom (y * (L ")) & [.(L . a),(L . b).] c= rng L & dom (x * (L ")) = dom (L ") & dom (y * (L ")) = dom (L ") & x * (L ") is differentiable & y * (L ") is differentiable & (x * (L ")) `| (dom (x * (L "))) is continuous & (y * (L ")) `| (dom (y * (L "))) is continuous & ( for s being Real st s in (dom (x * (L "))) /\ (dom (y * (L "))) holds
((diff ((x * (L ")),s)) ^2) + ((diff ((y * (L ")),s)) ^2) = 1 ) & integral ((y (#) (x `| (dom x))),a,b) = integral (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))),(L . a),(L . b)) ) by Th4;
B1: [.a,b.] c= ].a1,b1.[ by A2, XXREAL_1:47;
( a1 < a & a < b1 & a1 < b & b < b1 ) by A1, A2, XXREAL_0:2;
then ( a in ].a1,b1.[ & b in ].a1,b1.[ ) ;
then ( a in dom L & b in dom L ) by A2;
then B2: L . a < L . b by A1, A2;
then A3: ( L . a in [.(L . a),(L . b).] & L . b in [.(L . a),(L . b).] ) ;
A4: ( a in [.a,b.] & b in [.a,b.] ) by A1;
A5: (y * (L ")) . (L . a) = y . ((L ") . (L . a)) by A2, A3, FUNCT_1:13
.= 0 by A1, A2, A4, B1, FUNCT_1:34 ;
A6: (y * (L ")) . (L . b) = y . ((L ") . (L . b)) by A2, A3, FUNCT_1:13
.= 0 by A1, A2, A4, B1, FUNCT_1:34 ;
A7: ['(L . a),(L . b)'] = [.(L . a),(L . b).] by B2, INTEGRA5:def 3;
set x1 = x * (L ");
set y1 = y * (L ");
set a2 = L . a;
set b2 = L . b;
b in [.a,b.] by A1;
then A9: (ArcLenP (x,y,a,b)) . b = (L . b) - (L . a) by A2;
A14: (x * (L ")) . (L . a) = x . ((L ") . (L . a)) by A2, A3, FUNCT_1:13
.= x . a by A2, A4, B1, FUNCT_1:34 ;
thus integral ((y (#) (x `| (dom x))),a,b) <= ((1 / 2) * (l ^2)) / PI by A1, A2, A5, A6, A7, A9, B2, Lm3; :: thesis:

hereby :: thesis:

assume integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI ; :: thesis:

per cases by A1, A2, A5, A6, A7, A9, B2, Lm3;

suppose A16: for t being Real st t in [.(L . a),(L . b).] holds
( (y * (L ")) . t = (((L . b) - (L . a)) / PI) * (sin . ((PI * (t - (L . a))) / ((L . b) - (L . a)))) & (x * (L ")) . t = (((L . b) - (L . a)) / PI) * (((- (cos . ((PI * (t - (L . a))) / ((L . b) - (L . a))))) + (cos . 0)) + ((PI / ((L . b) - (L . a))) * ((x * (L ")) . (L . a)))) ) ; :: thesis:

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))) )

proof

let s be Real; :: thesis:
assume A17: s in [.a,b.] ; :: thesis:
then A19: L . s in [.(L . a),(L . b).] by A2, B1, FUNCT_1:def 6;
set t = L . s;
A23: (ArcLenP (x,y,a,b)) . s = (L . s) - (L . a) by A2, A17;
A24: (y * (L ")) . (L . s) = y . ((L ") . (L . s)) by A2, A19, FUNCT_1:13
.= y . s by A2, A17, B1, FUNCT_1:34 ;
(x * (L ")) . (L . s) = x . ((L ") . (L . s)) by A2, A19, FUNCT_1:13
.= x . s by A2, A17, B1, FUNCT_1:34 ;
hence ( 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))) ) by A1, A9, A14, A16, A19, A23, A24; :: thesis:

end;

hence ( 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))) ) ) ; :: thesis:

end;

suppose A25: for t being Real st t in [.(L . a),(L . b).] holds
( (y * (L ")) . t = - ((((L . b) - (L . a)) / PI) * (sin . ((PI * (t - (L . a))) / ((L . b) - (L . a))))) & (x * (L ")) . t = (((L . b) - (L . a)) / PI) * (((cos . ((PI * (t - (L . a))) / ((L . b) - (L . a)))) - (cos . 0)) + ((PI / ((L . b) - (L . a))) * ((x * (L ")) . (L . a)))) ) ; :: thesis:

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))) )

proof

let s be Real; :: thesis:
assume A26: s in [.a,b.] ; :: thesis:
then A27: L . s in [.(L . a),(L . b).] by A2, B1, FUNCT_1:def 6;
set t = L . s;
A31: (ArcLenP (x,y,a,b)) . s = (L . s) - (L . a) by A2, A26;
A32: (y * (L ")) . (L . s) = y . ((L ") . (L . s)) by A2, A27, FUNCT_1:13
.= y . s by A2, A26, B1, FUNCT_1:34 ;
(x * (L ")) . (L . s) = x . ((L ") . (L . s)) by A2, A27, FUNCT_1:13
.= x . s by A2, A26, B1, FUNCT_1:34 ;
hence ( 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))) ) by A1, A9, A14, A25, A27, A31, A32; :: thesis:

end;

assume ( 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))) ) ) ; :: thesis:

per cases ;

suppose A33: 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))) ) ; :: thesis:

for t being Real st t in [.(L . a),(L . b).] holds
( (y * (L ")) . t = (((L . b) - (L . a)) / PI) * (sin . ((PI * (t - (L . a))) / ((L . b) - (L . a)))) & (x * (L ")) . t = (((L . b) - (L . a)) / PI) * (((- (cos . ((PI * (t - (L . a))) / ((L . b) - (L . a))))) + (cos . 0)) + ((PI / ((L . b) - (L . a))) * ((x * (L ")) . (L . a)))) )

proof

let t be Real; :: thesis:
assume A34: t in [.(L . a),(L . b).] ; :: thesis:
then consider s being object such that
A35: ( s in dom L & s in [.a,b.] & t = L . s ) by A2, FUNCT_1:def 6;
A38: (ArcLenP (x,y,a,b)) . s = (L . s) - (L . a) by A2, A35;
A40: (y * (L ")) . t = y . ((L ") . (L . s)) by A2, A34, A35, FUNCT_1:13
.= y . s by A35, FUNCT_1:34 ;
(x * (L ")) . t = x . ((L ") . (L . s)) by A2, A34, A35, FUNCT_1:13
.= x . s by A35, FUNCT_1:34 ;
hence ( (y * (L ")) . t = (((L . b) - (L . a)) / PI) * (sin . ((PI * (t - (L . a))) / ((L . b) - (L . a)))) & (x * (L ")) . t = (((L . b) - (L . a)) / PI) * (((- (cos . ((PI * (t - (L . a))) / ((L . b) - (L . a))))) + (cos . 0)) + ((PI / ((L . b) - (L . a))) * ((x * (L ")) . (L . a)))) ) by A1, A9, A14, A33, A35, A38, A40; :: thesis:

end;

hence integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI by A1, A2, A5, A6, A7, A9, B2, Lm3; :: thesis:

end;

suppose A41: 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))) ) ; :: thesis:

for t being Real st t in [.(L . a),(L . b).] holds
( (y * (L ")) . t = - ((((L . b) - (L . a)) / PI) * (sin . ((PI * (t - (L . a))) / ((L . b) - (L . a))))) & (x * (L ")) . t = (((L . b) - (L . a)) / PI) * (((cos . ((PI * (t - (L . a))) / ((L . b) - (L . a)))) - (cos . 0)) + ((PI / ((L . b) - (L . a))) * ((x * (L ")) . (L . a)))) )

proof

let t be Real; :: thesis:
assume A42: t in [.(L . a),(L . b).] ; :: thesis:
then consider s being object such that
A43: ( s in dom L & s in [.a,b.] & t = L . s ) by A2, FUNCT_1:def 6;
A44: ( 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))) ) by A41, A43;
A48: (y * (L ")) . t = y . ((L ") . (L . s)) by A2, A42, A43, FUNCT_1:13
.= y . s by A43, FUNCT_1:34 ;
(x * (L ")) . t = x . ((L ") . (L . s)) by A2, A42, A43, FUNCT_1:13
.= x . s by A43, FUNCT_1:34 ;
hence ( (y * (L ")) . t = - ((((L . b) - (L . a)) / PI) * (sin . ((PI * (t - (L . a))) / ((L . b) - (L . a))))) & (x * (L ")) . t = (((L . b) - (L . a)) / PI) * (((cos . ((PI * (t - (L . a))) / ((L . b) - (L . a)))) - (cos . 0)) + ((PI / ((L . b) - (L . a))) * ((x * (L ")) . (L . a)))) ) by A1, A2, A9, A14, A43, A44, A48; :: thesis:

end;

hence integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * (l ^2)) / PI by A1, A2, A5, A6, A7, A9, B2, Lm3; :: thesis:

end;