theorem Th4: :: CURVE:4

for a, b being Real
for x, y being PartFunc of REAL,REAL st a < b & 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
ex a1, b1 being Real ex L being one-to-one PartFunc of REAL,REAL st
( 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)) )