theorem Th3: :: CURVE:3

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 PartFunc of REAL,REAL ex Z being open Subset of REAL st
( a1 < a & b < b1 & Z = (dom x) /\ (dom y) & [.a,b.] c= ].a1,b1.[ & [.a1,b1.] c= Z & dom l = Z & ( 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) ) & l is_differentiable_on ].a1,b1.[ & l `| ].a1,b1.[ = ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ].a1,b1.[ & l `| ].a1,b1.[ is continuous & ( for t being Real st t in ].a1,b1.[ holds
( l is_differentiable_in t & diff (l,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) ) ) & ( for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = (l . t) - (l . a) ) )