:: deftheorem Def1 defines ArcLenP CURVE:def 1 :
for a, b being Real
for x, y, b₅ being PartFunc of REAL,REAL holds
( b₅ = ArcLenP (x,y,a,b) iff ( dom b₅ = [.a,b.] & ( for t being Real st t in [.a,b.] holds
b₅ . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t) ) ) );