let a, b be Real; :: thesis:
let x, y be PartFunc of REAL,REAL; :: thesis:
assume A1: ( 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) ) ) ; :: thesis:
reconsider Z1 = dom x, Z2 = dom y as open Subset of REAL by A1, FDIFF_1:10;
reconsider Z = Z1 /\ Z2 as open Subset of REAL ;
A3: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A4: ( Z c= Z1 & Z c= Z2 ) by XBOOLE_1:17;
A5: ['a,b'] c= Z by A1, A3, XBOOLE_1:19;
a in [.a,b.] by A1;
then consider d1 being Real such that
A6: ( 0 < d1 & ].(a - d1),(a + d1).[ c= Z ) by A3, A5, RCOMP_1:19;
b in [.a,b.] by A1;
then consider d2 being Real such that
A7: ( 0 < d2 & ].(b - d2),(b + d2).[ c= Z ) by A3, A5, RCOMP_1:19;
reconsider d = min (d1,d2) as Real ;
A8: ( d <= d1 & d <= d2 ) by XXREAL_0:17;
B8: 0 < d by A6, A7, XXREAL_0:15;
then A9: ( 0 < d / 2 & d / 2 < d ) by XREAL_1:216;
set a1 = a - (d / 2);
set b1 = b + (d / 2);
A10: a - (d / 2) < a - 0 by B8, XREAL_1:15;
then A11: a - (d / 2) < b by A1, XXREAL_0:2;
A12: b + 0 < b + (d / 2) by B8, XREAL_1:8;
then A13: a - (d / 2) < b + (d / 2) by A11, XXREAL_0:2;
A14: ['(a - (d / 2)),(b + (d / 2))'] = [.(a - (d / 2)),(b + (d / 2)).] by A11, A12, INTEGRA5:def 3, XXREAL_0:2;
A15: [.(a - (d / 2)),(b + (d / 2)).] c= Z

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A16: t in [.(a - (d / 2)),(b + (d / 2)).] ; :: thesis:
then reconsider s = t as Real ;

per cases by A16, XXREAL_1:1;

suppose A17: ( a - (d / 2) <= s & s < a ) ; :: thesis:

A18: a - d < a - (d / 2) by A9, XREAL_1:15;
a - d1 <= a - d by A8, XREAL_1:13;
then a - d1 < a - (d / 2) by A18, XXREAL_0:2;
then A19: a - d1 < s by A17, XXREAL_0:2;
a + 0 < a + d1 by A6, XREAL_1:8;
then s < a + d1 by A17, XXREAL_0:2;
then t in ].(a - d1),(a + d1).[ by A19;
hence t in Z by A6; :: thesis:

end;

suppose ( a <= s & s <= b ) ; :: thesis:

then t in [.a,b.] ;
hence t in Z by A3, A5; :: thesis:

end;

suppose A20: ( b < s & s <= b + (d / 2) ) ; :: thesis:

A21: b + (d / 2) < b + d by A9, XREAL_1:8;
b + d <= b + d2 by A8, XREAL_1:7;
then b + (d / 2) < b + d2 by A21, XXREAL_0:2;
then A22: s < b + d2 by A20, XXREAL_0:2;
b - d2 < b - 0 by A7, XREAL_1:15;
then b - d2 < s by A20, XXREAL_0:2;
then t in ].(b - d2),(b + d2).[ by A22;
hence t in Z by A7; :: thesis:

end;

deffunc H₁( Real) -> Element of REAL = In ((integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),$1)),REAL);
consider l0 being Function of REAL,REAL such that
A26: for t being Element of REAL holds l0 . t = H₁(t) from FUNCT_2:sch 4();
A27: for t being Real holds l0 . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),t)

proof

end;

now :: thesis:

let w be object ; :: thesis:
assume A33: w in rng (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) ; :: thesis:
then consider t being object such that
A34: ( t in dom (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) & w = (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) . t ) by FUNCT_1:def 3;
reconsider v = w as Real by A33;
reconsider s = t as Real by A34;
w = (((x `| (dom x)) (#) (x `| (dom x))) . s) + (((y `| (dom y)) (#) (y `| (dom y))) . s) by VALUED_1:def 1, A34
.= (((x `| (dom x)) . s) * ((x `| (dom x)) . s)) + (((y `| (dom y)) (#) (y `| (dom y))) . s) by VALUED_1:5
.= (((x `| (dom x)) . s) ^2) + (((y `| (dom y)) . s) ^2) by VALUED_1:5
.= ((diff (x,s)) ^2) + (((y `| (dom y)) . s) ^2) by A1, A4, A32, A34, FDIFF_1:def 7
.= ((diff (x,s)) ^2) + ((diff (y,s)) ^2) by A1, A4, A32, A34, FDIFF_1:def 7 ;
then A36: 0 < v by A1, A34, A32;
v < +infty by XREAL_0:def 1, XXREAL_0:9;
then w in ].0,+infty.[ by A36;
hence w in dom (#R (1 / 2)) by TAYLOR_1:def 4; :: thesis:

end;

now :: thesis:

let t be Real; :: thesis:
assume t in dom (#R (1 / 2)) ; :: thesis:
then t in ].0,+infty.[ by TAYLOR_1:def 4;
then ( 0 < t & t < +infty ) by XXREAL_1:4;
hence #R (1 / 2) is_continuous_in t by FDIFF_1:24, TAYLOR_1:21; :: thesis:

end;

then A38: #R (1 / 2) is continuous ;
then A39: (#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) is continuous by A1;
((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ['(a - (d / 2)),(b + (d / 2))'] is continuous by A1, A38;
then A40: ( ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ['(a - (d / 2)),(b + (d / 2))'] is bounded & (#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) is_integrable_on ['(a - (d / 2)),(b + (d / 2))'] ) by A14, A15, A37, INTEGRA5:10, INTEGRA5:11;
take a - (d / 2) ; :: thesis:
take b + (d / 2) ; :: thesis:
take l ; :: thesis:
take Z ; :: thesis:
thus ( a - (d / 2) < a & b < b + (d / 2) ) by A10, A12; :: thesis:
thus Z = (dom x) /\ (dom y) ; :: thesis:
thus [.a,b.] c= ].(a - (d / 2)),(b + (d / 2)).[ by A10, A12, XXREAL_1:47; :: thesis:
thus [.(a - (d / 2)),(b + (d / 2)).] c= Z by A15; :: thesis:
thus dom l = Z by A28, RELAT_1:62; :: thesis:
thus A42: for t being Real st t in [.(a - (d / 2)),(b + (d / 2)).] holds
l . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),t) :: thesis:

proof

let t be Real; :: thesis:
assume t in [.(a - (d / 2)),(b + (d / 2)).] ; :: thesis:
hence l . t = l0 . t by A15, FUNCT_1:49
.= integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),t) by A27 ;
:: thesis:

end;

A43: [.a,b.] c= ].(a - (d / 2)),(b + (d / 2)).[ by A10, A12, XXREAL_1:47;
Z1: ].(a - (d / 2)),(b + (d / 2)).[ c= [.(a - (d / 2)),(b + (d / 2)).] by Lm1;
Z2: a in [.a,b.] by A1;
A56: for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = (l . t) - (l . a)

proof

let t be Real; :: thesis:
assume A57: t in [.a,b.] ; :: thesis:
then A59: ( l . a = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),a) & l . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),t) ) by Z1, A42, Z2, A43;
A60: ( a <= t & t <= b ) by A57, XXREAL_1:1;
then A61: a - (d / 2) < t by A10, XXREAL_0:2;
Z5: t <= b + (d / 2) by A12, A60, XXREAL_0:2;
A66: ['(a - (d / 2)),t'] c= dom ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A62: z in ['(a - (d / 2)),t'] ; :: thesis:
then A63: z in [.(a - (d / 2)),t.] by A10, A60, INTEGRA5:def 3, XXREAL_0:2;
reconsider s = z as Real by A62;
( a - (d / 2) <= s & s <= t ) by A63, XXREAL_1:1;
then ( a - (d / 2) <= s & s <= b + (d / 2) ) by Z5, XXREAL_0:2;
then s in [.(a - (d / 2)),(b + (d / 2)).] ;
hence z in dom ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) by A15, A37; :: thesis:

end;

((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ['(a - (d / 2)),t'] is continuous by A1, A38;
then A67: ( ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ['(a - (d / 2)),t'] is bounded & (#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) is_integrable_on ['(a - (d / 2)),t'] ) by A66, INTEGRA5:10, INTEGRA5:11;
Z4: ( a - (d / 2) < a & a < b + (d / 2) ) by Z2, A43, XXREAL_1:4;
( a - (d / 2) < a & a <= t ) by A57, XXREAL_1:1, A10;
then a in [.(a - (d / 2)),t.] ;
then a in ['(a - (d / 2)),t'] by A60, Z4, INTEGRA5:def 3, XXREAL_0:2;
then l . t = (l . a) + (integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a,t)) by A59, A61, A66, A67, INTEGRA6:17;
hence (ArcLenP (x,y,a,b)) . t = (l . t) - (l . a) by A57, Def1; :: thesis:

end;

A70: for t being Real st t in ].(a - (d / 2)),(b + (d / 2)).[ holds
l . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),(a - (d / 2)),t) by Z1, A42;
A75: ].(a - (d / 2)),(b + (d / 2)).[ c= dom l by Z1, A15, A29;

A72: now :: thesis:

let t be Real; :: thesis:
assume A73: t in ].(a - (d / 2)),(b + (d / 2)).[ ; :: thesis:
(#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) is_continuous_in t by Z1, A15, A37, A39, A73;
hence ( l is_differentiable_in t & diff (l,t) = ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) . t ) by A13, A14, A15, A30, A37, A40, A70, A73, INTEGRA6:28; :: thesis:

end;

for t being Real st t in ].(a - (d / 2)),(b + (d / 2)).[ holds
l is_differentiable_in t by A72;
hence A76: l is_differentiable_on ].(a - (d / 2)),(b + (d / 2)).[ by A75, FDIFF_1:9; :: thesis:
then A77: dom (l `| ].(a - (d / 2)),(b + (d / 2)).[) = ].(a - (d / 2)),(b + (d / 2)).[ by FDIFF_1:def 7;
A78: dom (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ].(a - (d / 2)),(b + (d / 2)).[) = ].(a - (d / 2)),(b + (d / 2)).[ by A29, A37, A75, RELAT_1:62;

now :: thesis:

end;

hence ( l `| ].(a - (d / 2)),(b + (d / 2)).[ = ((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) | ].(a - (d / 2)),(b + (d / 2)).[ & l `| ].(a - (d / 2)),(b + (d / 2)).[ is continuous ) by A1, A38, A77, A78, FUNCT_1:2; :: thesis:
thus for t being Real st t in ].(a - (d / 2)),(b + (d / 2)).[ holds
( l is_differentiable_in t & diff (l,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) ) :: thesis:

proof

let t be Real; :: thesis:
assume A80: t in ].(a - (d / 2)),(b + (d / 2)).[ ; :: thesis:
A81: ].(a - (d / 2)),(b + (d / 2)).[ c= [.(a - (d / 2)),(b + (d / 2)).] by Lm1;
then t in Z by A15, A80;
then ( t in dom x & t in dom y ) by XBOOLE_0:def 4;
then A84: ( (x `| (dom x)) . t = diff (x,t) & (y `| (dom y)) . t = diff (y,t) ) by A1, FDIFF_1:def 7;
A83: (#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) is_continuous_in t by A15, A37, A39, A80, A81;
A85: (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) . t = (((x `| (dom x)) (#) (x `| (dom x))) . t) + (((y `| (dom y)) (#) (y `| (dom y))) . t) by A15, A32, A80, A81, VALUED_1:def 1
.= (((x `| (dom x)) . t) * ((x `| (dom x)) . t)) + (((y `| (dom y)) (#) (y `| (dom y))) . t) by VALUED_1:5
.= ((diff (x,t)) ^2) + ((diff (y,t)) ^2) by A84, VALUED_1:5 ;
then A86: 0 < (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) . t by A1, A15, A80, A81;
(((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) . t < +infty by XREAL_0:def 1, XXREAL_0:9;
then A87: (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) . t in right_open_halfline 0 by A86;
((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))) . t = (#R (1 / 2)) . ((((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y)))) . t) by A15, A37, A80, A81, FUNCT_1:12
.= (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) by A85, A87, TAYLOR_1:def 4 ;
hence ( l is_differentiable_in t & diff (l,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) ) by A13, A14, A15, A30, A37, A40, A70, A80, A83, INTEGRA6:28; :: thesis:

end;

thus for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = (l . t) - (l . a) by A56; :: thesis: