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:
then consider a1, b1 being Real, l being PartFunc of REAL,REAL, Z being open Subset of REAL such that
A2: ( 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) ) ) by Th3;
set L = l | ].a1,b1.[;
B5: ].a1,b1.[ c= [.a1,b1.] by Lm1;
A5: dom (l | ].a1,b1.[) = ].a1,b1.[ by A2, RELAT_1:62;
A6: for t being Real st t in ].a1,b1.[ holds
(l | ].a1,b1.[) . t = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a1,t)

end;

A9: ( a in [.a,b.] & b in [.a,b.] ) by A1;
A10: for t being Real st t in [.a,b.] holds
(ArcLenP (x,y,a,b)) . t = ((l | ].a1,b1.[) . t) - ((l | ].a1,b1.[) . a)

proof

let t be Real; :: thesis:
assume A11: t in [.a,b.] ; :: thesis:
hence (ArcLenP (x,y,a,b)) . t = (l . t) - (l . a) by A2
.= ((l | ].a1,b1.[) . t) - (l . a) by A2, A11, FUNCT_1:49
.= ((l | ].a1,b1.[) . t) - ((l | ].a1,b1.[) . a) by A2, A9, FUNCT_1:49 ;
:: thesis:

end;

A13: for t being Real st t in ].a1,b1.[ holds
0 < diff (l,t)

proof

let t be Real; :: thesis:
assume A14: t in ].a1,b1.[ ; :: thesis:
then diff (l,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) by A2;
hence 0 < diff (l,t) by A1, A2, A14, PREPOWER:81; :: thesis:

end;

then A16: l | ].a1,b1.[ is increasing by A2, ROLLE:9;

now :: thesis:

let t1, t2 be object ; :: thesis:
assume A17: ( t1 in dom (l | ].a1,b1.[) & t2 in dom (l | ].a1,b1.[) & (l | ].a1,b1.[) . t1 = (l | ].a1,b1.[) . t2 ) ; :: thesis:
then reconsider s1 = t1, s2 = t2 as Real ;
thus t1 = t2 :: thesis:

proof

assume t1 <> t2 ; :: thesis:

per cases by XXREAL_0:1;

suppose s1 < s2 ; :: thesis:

hence contradiction by A16, A17; :: thesis:

end;

suppose s2 < s1 ; :: thesis:

hence contradiction by A16, A17; :: thesis:

end;

then reconsider L = l | ].a1,b1.[ as one-to-one PartFunc of REAL,REAL by FUNCT_1:def 4;
set P = integral (((#R (1 / 2)) * (((x `| (dom x)) (#) (x `| (dom x))) + ((y `| (dom y)) (#) (y `| (dom y))))),a1,b1);
A19: L is_differentiable_on ].a1,b1.[ by A2, RELAT_1:62;
A20: for t being Real st t in ].a1,b1.[ holds
diff (L,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2)

proof

let t be Real; :: thesis:
assume A21: t in ].a1,b1.[ ; :: thesis:
then diff (l,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) by A2;
hence diff (L,t) = (((diff (x,t)) ^2) + ((diff (y,t)) ^2)) #R (1 / 2) by A2, A21, PDLAX:11; :: thesis:

end;

A23: for t being Real st t in ].a1,b1.[ holds
0 < diff (L,t)

proof

let t be Real; :: thesis:
assume A24: t in ].a1,b1.[ ; :: thesis:
then 0 < diff (l,t) by A13;
hence 0 < diff (L,t) by A2, A24, PDLAX:11; :: thesis:

end;

A27: ( L is one-to-one & L " is_differentiable_on dom (L ") & ( for t being Real st t in dom (L ") holds
diff ((L "),t) = 1 / (diff (L,((L ") . t))) ) ) by A19, A23, FDIFF_2:48;
A28: dom (L ") = rng L by FUNCT_1:33;
A30: 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 )

proof

let s be Real; :: thesis:
assume A31: s in rng L ; :: thesis:
then A33: L " is_differentiable_in s by A27, A28;
(L ") . s in rng (L ") by A28, A31, FUNCT_1:3;
then A34: (L ") . s in ].a1,b1.[ by A5, FUNCT_1:33;
then A36: ( (L ") . s in dom x & (L ") . s in dom y ) by A2, XBOOLE_0:def 4;
( x is_differentiable_on dom x & y is_differentiable_on dom y ) by A1;
then A37: ( x is_differentiable_in (L ") . s & y is_differentiable_in (L ") . s ) by A36;
hence ( x * (L ") is_differentiable_in s & y * (L ") is_differentiable_in s ) by A33, FDIFF_2:13; :: thesis:
thus A38: ( diff ((x * (L ")),s) = (diff (x,((L ") . s))) * (diff ((L "),s)) & diff ((y * (L ")),s) = (diff (y,((L ") . s))) * (diff ((L "),s)) ) by A33, A37, FDIFF_2:13; :: thesis:
A39: diff ((L "),s) = 1 / (diff (L,((L ") . s))) by A19, A23, A28, A31, FDIFF_2:48;
A40: diff (L,((L ") . s)) = (((diff (x,((L ") . s))) ^2) + ((diff (y,((L ") . s))) ^2)) #R (1 / 2) by A20, A34;
A41: 0 < ((diff (x,((L ") . s))) ^2) + ((diff (y,((L ") . s))) ^2) by A1, A2, A34;
A42: (diff (L,((L ") . s))) ^2 = (((diff (x,((L ") . s))) ^2) + ((diff (y,((L ") . s))) ^2)) #R ((1 / 2) + (1 / 2)) by A1, A2, A34, A40, PREPOWER:75
.= ((diff (x,((L ") . s))) ^2) + ((diff (y,((L ") . s))) ^2) by A1, A2, A34, PREPOWER:72 ;
thus ((diff ((x * (L ")),s)) ^2) + ((diff ((y * (L ")),s)) ^2) = (((diff (x,((L ") . s))) ^2) + ((diff (y,((L ") . s))) ^2)) * ((1 / (diff (L,((L ") . s)))) * (1 / (diff (L,((L ") . s))))) by A38, A39
.= (((diff (x,((L ") . s))) ^2) + ((diff (y,((L ") . s))) ^2)) * ((1 * 1) / ((diff (L,((L ") . s))) * (diff (L,((L ") . s))))) by XCMPLX_1:76
.= 1 by A41, A42, XCMPLX_1:106 ; :: thesis:

end;

A43: rng (L ") = ].a1,b1.[ by A5, FUNCT_1:33;
( (dom x) /\ (dom y) c= dom x & (dom x) /\ (dom y) c= dom y ) by XBOOLE_1:17;
then A45: ( ].a1,b1.[ c= dom x & ].a1,b1.[ c= dom y ) by A2;
then A47: ( dom (x * (L ")) = dom (L ") & dom (y * (L ")) = dom (L ") ) by A43, RELAT_1:27;
then A49: x * (L ") is_differentiable_on dom (x * (L ")) by A28, A30;
A51: y * (L ") is_differentiable_on dom (y * (L ")) by A28, A30, A47;

A52: now :: thesis:

let t be object ; :: thesis:
assume A53: t in dom (L ") ; :: thesis:
then reconsider s = t as Real ;
(L ") . s in rng (L ") by A53, FUNCT_1:3;
then (L ") . s in dom L by FUNCT_1:33;
then A55: ( (L ") . s in dom x & (L ") . s in dom y ) by A2, A5, XBOOLE_0:def 4;
thus ((x * (L ")) `| (dom (x * (L ")))) . t = diff ((x * (L ")),s) by FDIFF_1:def 7, A47, A53, A49
.= (diff (x,((L ") . s))) * (diff ((L "),s)) by A28, A30, A53
.= ((x `| (dom x)) . ((L ") . s)) * (diff ((L "),s)) by A1, A55, FDIFF_1:def 7
.= ((x `| (dom x)) . ((L ") . s)) * (((L ") `| (dom (L "))) . s) by A27, A53, FDIFF_1:def 7
.= (((x `| (dom x)) * (L ")) . s) * (((L ") `| (dom (L "))) . s) by A53, FUNCT_1:13
.= (((x `| (dom x)) * (L ")) (#) ((L ") `| (dom (L ")))) . t by VALUED_1:5 ; :: thesis:
thus ((y * (L ")) `| (dom (y * (L ")))) . t = diff ((y * (L ")),s) by A47, A51, A53, FDIFF_1:def 7
.= (diff (y,((L ") . s))) * (diff ((L "),s)) by A28, A30, A53
.= ((y `| (dom y)) . ((L ") . s)) * (diff ((L "),s)) by A1, A55, FDIFF_1:def 7
.= ((y `| (dom y)) . ((L ") . s)) * (((L ") `| (dom (L "))) . s) by A27, A53, FDIFF_1:def 7
.= (((y `| (dom y)) * (L ")) . s) * (((L ") `| (dom (L "))) . s) by A53, FUNCT_1:13
.= (((y `| (dom y)) * (L ")) (#) ((L ") `| (dom (L ")))) . t by VALUED_1:5 ; :: thesis:

end;

( dom (x `| (dom x)) = dom x & dom (y `| (dom y)) = dom y ) by A1, FDIFF_1:def 7;
then A56: ( dom ((x `| (dom x)) * (L ")) = dom (L ") & dom ((y `| (dom y)) * (L ")) = dom (L ") ) by A43, A45, RELAT_1:27;
A57: dom (((x `| (dom x)) * (L ")) (#) ((L ") `| (dom (L ")))) = (dom ((x `| (dom x)) * (L "))) /\ (dom ((L ") `| (dom (L ")))) by VALUED_1:def 4
.= (dom (L ")) /\ (dom (L ")) by A27, A56, FDIFF_1:def 7
.= dom (L ") ;
A58: ( dom ((x * (L ")) `| (dom (x * (L ")))) = dom (L ") & dom ((y * (L ")) `| (dom (y * (L ")))) = dom (L ") ) by A47, A49, A51, FDIFF_1:def 7;
then A59: for t being object st t in dom ((x * (L ")) `| (dom (x * (L ")))) holds
((x * (L ")) `| (dom (x * (L ")))) . t = (((x `| (dom x)) * (L ")) (#) ((L ") `| (dom (L ")))) . t by A52;
A60: dom (((y `| (dom y)) * (L ")) (#) ((L ") `| (dom (L ")))) = (dom ((y `| (dom y)) * (L "))) /\ (dom ((L ") `| (dom (L ")))) by VALUED_1:def 4
.= (dom (L ")) /\ (dom (L ")) by A27, A56, FDIFF_1:def 7
.= dom (L ") ;
A61: for t being object st t in dom ((y * (L ")) `| (dom (y * (L ")))) holds
((y * (L ")) `| (dom (y * (L ")))) . t = (((y `| (dom y)) * (L ")) (#) ((L ") `| (dom (L ")))) . t by A52, A58;
A62: L " is continuous by A27, FDIFF_1:25;
set LL = (L ") `| (dom (L "));
dom (L `| (dom L)) = dom L by A19, A5, FDIFF_1:def 7
.= rng (L ") by FUNCT_1:33 ;
then A63: dom ((L `| (dom L)) * (L ")) = dom (L ") by RELAT_1:27;
((L `| (dom L)) * (L ")) " {0} = {}

proof

assume ((L `| (dom L)) * (L ")) " {0} <> {} ; :: thesis:
then consider z being object such that
A64: z in ((L `| (dom L)) * (L ")) " {0} ;
A65: ( z in dom ((L `| (dom L)) * (L ")) & ((L `| (dom L)) * (L ")) . z in {0} ) by A64, FUNCT_1:def 7;
A66: ((L `| (dom L)) * (L ")) . z = 0 by A65, TARSKI:def 1;
reconsider t = z as Real by A64;
(L ") . t in rng (L ") by A63, A65, FUNCT_1:3;
then A67: (L ") . t in ].a1,b1.[ by A5, FUNCT_1:33;
A68: ((L `| (dom L)) * (L ")) . t = (L `| (dom L)) . ((L ") . t) by A63, A65, FUNCT_1:13
.= diff (L,((L ") . t)) by A5, A19, A67, FDIFF_1:def 7 ;
diff (L,((L ") . t)) = (((diff (x,((L ") . t))) ^2) + ((diff (y,((L ") . t))) ^2)) #R (1 / 2) by A20, A67;
hence contradiction by A1, A2, A66, A67, A68, PREPOWER:81; :: thesis:

end;

then A69: dom (((L `| (dom L)) * (L ")) ^) = (dom (L ")) \ {} by A63, RFUNCT_1:def 2
.= dom (L ") ;
A70: dom ((L ") `| (dom (L "))) = dom (L ") by A27, FDIFF_1:def 7;

A71: now :: thesis:

let s be object ; :: thesis:
assume A73: s in dom ((L ") `| (dom (L "))) ; :: thesis:
then reconsider t = s as Real ;
A74: ((L ") `| (dom (L "))) . s = diff ((L "),t) by A27, A70, A73, FDIFF_1:def 7
.= 1 / (diff (L,((L ") . t))) by A19, A23, A70, A73, FDIFF_2:48 ;
(L ") . t in rng (L ") by A70, A73, FUNCT_1:3;
then A75: (L ") . t in ].a1,b1.[ by A5, FUNCT_1:33;
((L `| (dom L)) * (L ")) . t = (L `| (dom L)) . ((L ") . t) by A70, A73, FUNCT_1:13
.= diff (L,((L ") . t)) by A5, A19, A75, FDIFF_1:def 7 ;
hence ((L ") `| (dom (L "))) . s = (((L `| (dom L)) * (L ")) ^) . s by A69, A70, A73, A74, RFUNCT_1:def 2; :: thesis:

end;

proof

let t be Real; :: thesis:
assume A79: t in dom ((L ") `| (dom (L "))) ; :: thesis:
then (L ") . t in rng (L ") by A70, FUNCT_1:3;
then A80: (L ") . t in ].a1,b1.[ by A5, FUNCT_1:33;
A81: ((L `| (dom L)) * (L ")) . t = (L `| (dom L)) . ((L ") . t) by A70, A79, FUNCT_1:13
.= diff (L,((L ") . t)) by A5, A19, A80, FDIFF_1:def 7 ;
diff (L,((L ") . t)) = (((diff (x,((L ") . t))) ^2) + ((diff (y,((L ") . t))) ^2)) #R (1 / 2) by A20, A80;
then ((L `| (dom L)) * (L ")) . t <> 0 by A1, A2, A80, A81, PREPOWER:81;
hence (L ") `| (dom (L ")) is_continuous_in t by A63, A70, A76, A77, A79, FCONT_1:10; :: thesis:

end;

then A84: (L ") `| (dom (L ")) is continuous ;
then A85: (x * (L ")) `| (dom (x * (L "))) is continuous by A1, A57, A58, A59, A62, FUNCT_1:2;
take a1 ; :: thesis:
take b1 ; :: thesis:
take L ; :: thesis:
A94: [.a,b.] c= dom L by A2, RELAT_1:62;
A86: for s being object holds
( s in L .: [.a,b.] iff s in [.(L . a),(L . b).] )

proof

let s be object ; :: thesis:

hereby :: thesis:

assume s in L .: [.a,b.] ; :: thesis:
then consider x being object such that
A87: ( x in dom L & x in [.a,b.] & s = L . x ) by FUNCT_1:def 6;
reconsider t = x as Real by A87;
A88: ( a <= t & t <= b ) by A87, XXREAL_1:1;
A91: L . a <= L . t

proof

per cases ;

suppose a = t ; :: thesis:

hence L . a <= L . t ; :: thesis:

end;

suppose a <> t ; :: thesis:

then a < t by A88, XXREAL_0:1;
hence L . a <= L . t by A16, A87, A94, A9; :: thesis:

end;

L . t <= L . b

proof

per cases ;

suppose b = t ; :: thesis:

hence L . t <= L . b ; :: thesis:

end;

suppose b <> t ; :: thesis:

then t < b by A88, XXREAL_0:1;
hence L . t <= L . b by A16, A87, A94, A9; :: thesis:

end;

hence s in [.(L . a),(L . b).] by A87, A91; :: thesis:

end;

assume A93: s in [.(L . a),(L . b).] ; :: thesis:
then reconsider t = s as Real ;

per cases by A93, XXREAL_1:1;

suppose L . a = t ; :: thesis:

hence s in L .: [.a,b.] by A94, A9, FUNCT_1:def 6; :: thesis:

end;

suppose ( L . a <> t & L . a <= t & t <= L . b & L . b <> t ) ; :: thesis:

then A100: ( L . a < t & t < L . b ) by XXREAL_0:1;
L | ].a1,b1.[ is continuous by A2, FDIFF_1:25;
then L | [.a,b.] is continuous ;
then consider u being Real such that
A101: ( a < u & u < b & t = L . u ) by A1, A94, A100, Th1;
u in [.a,b.] by A101;
hence s in L .: [.a,b.] by A94, A101, FUNCT_1:def 6; :: thesis:

end;

suppose L . b = t ; :: thesis:

hence s in L .: [.a,b.] by A94, A9, FUNCT_1:def 6; :: thesis:

end;

A104: L | ].a1,b1.[ is continuous by A2, FDIFF_1:25;
set e1 = (a - a1) / 2;
set e2 = (b1 - b) / 2;
B104: ( 0 < a - a1 & 0 < b1 - b ) by A2, XREAL_1:50;
then A105: ( 0 < (a - a1) / 2 & (a - a1) / 2 < a - a1 & 0 < (b1 - b) / 2 & (b1 - b) / 2 < b1 - b ) by XREAL_1:216;
set a2 = a1 + ((a - a1) / 2);
set b2 = b1 - ((b1 - b) / 2);
set H = (y * (L ")) (#) ((x `| (dom x)) * (L "));
A106: ( a1 + ((a - a1) / 2) < a & a1 + ((a - a1) / 2) < b & b < b1 - ((b1 - b) / 2) & a1 + ((a - a1) / 2) < b1 - ((b1 - b) / 2) & [.a,b.] c= ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ & [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] c= ].a1,b1.[ )

proof

A107: a1 + ((a - a1) / 2) < a1 + (a - a1) by A105, XREAL_1:8;
hence a1 + ((a - a1) / 2) < a ; :: thesis:
thus A108: a1 + ((a - a1) / 2) < b by A1, A107, XXREAL_0:2; :: thesis:
A109: b1 - (b1 - b) < b1 - ((b1 - b) / 2) by A105, XREAL_1:15;
hence ( b < b1 - ((b1 - b) / 2) & a1 + ((a - a1) / 2) < b1 - ((b1 - b) / 2) ) by A108, XXREAL_0:2; :: thesis:
thus [.a,b.] c= ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ by A107, A109, XXREAL_1:47; :: thesis:
A111: a1 + 0 < a1 + ((a - a1) / 2) by B104, XREAL_1:8;
b1 - ((b1 - b) / 2) < b1 - 0 by B104, XREAL_1:15;
hence [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] c= ].a1,b1.[ by A111, XXREAL_1:47; :: thesis:

end;

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

proof

let t be Real; :: thesis:
t in REAL by XREAL_0:def 1;
then F0 . t = In ((integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),t)),REAL) by A114;
hence F0 . t = integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),t) ; :: thesis:

end;

set F = F0 | [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).];
dom F0 = REAL by FUNCT_2:def 1;
then A116: dom (F0 | [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).]) = [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by RELAT_1:62;
reconsider F = F0 | [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] as PartFunc of REAL,REAL ;
A0: ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ c= [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by Lm1;
A117: for t being Real st t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ holds
F . t = integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),t)

proof

let t be Real; :: thesis:
assume t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ ; :: thesis:
hence F . t = F0 . t by A0, FUNCT_1:49
.= integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),t) by A115 ;
:: thesis:

end;

B118: y | (dom y) is continuous by A1, FDIFF_1:25;
then A119: y (#) (x `| (dom x)) is continuous by A1;
A120: (y (#) (x `| (dom x))) | ['(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2))'] is continuous by A1, B118;
A121: dom (y (#) (x `| (dom x))) = (dom y) /\ (dom (x `| (dom x))) by VALUED_1:def 4
.= Z by A1, A2, FDIFF_1:def 7 ;
A122: ['(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2))'] c= dom (y (#) (x `| (dom x)))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in ['(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2))'] ; :: thesis:
then z in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A106, INTEGRA5:def 3;
hence z in dom (y (#) (x `| (dom x))) by A2, B5, A106, A121; :: thesis:

end;

then A123: ( (y (#) (x `| (dom x))) | ['(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2))'] is bounded & y (#) (x `| (dom x)) is_integrable_on ['(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2))'] ) by A120, INTEGRA5:10, INTEGRA5:11;
A124: ( F . a = integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),a) & F . b = integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),b) ) by A9, A106, A117;
A126: ['(a1 + ((a - a1) / 2)),b'] c= dom (y (#) (x `| (dom x)))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume B124: z in ['(a1 + ((a - a1) / 2)),b'] ; :: thesis:
then A125: z in [.(a1 + ((a - a1) / 2)),b.] by A106, INTEGRA5:def 3;
reconsider t = z as Real by B124;
( a1 + ((a - a1) / 2) <= t & t <= b ) by A125, XXREAL_1:1;
then ( a1 + ((a - a1) / 2) <= t & t <= b1 - ((b1 - b) / 2) ) by A106, XXREAL_0:2;
then t in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] ;
then t in ['(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2))'] by A106, INTEGRA5:def 3;
hence z in dom (y (#) (x `| (dom x))) by A122; :: thesis:

end;

(y (#) (x `| (dom x))) | ['(a1 + ((a - a1) / 2)),b'] is continuous by A1, B118;
then A127: ( (y (#) (x `| (dom x))) | ['(a1 + ((a - a1) / 2)),b'] is bounded & y (#) (x `| (dom x)) is_integrable_on ['(a1 + ((a - a1) / 2)),b'] ) by A126, INTEGRA5:10, INTEGRA5:11;
a in [.(a1 + ((a - a1) / 2)),b.] by A1, A106;
then a in ['(a1 + ((a - a1) / 2)),b'] by A106, INTEGRA5:def 3;
then A129: integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),b) = (integral ((y (#) (x `| (dom x))),(a1 + ((a - a1) / 2)),a)) + (integral ((y (#) (x `| (dom x))),a,b)) by A106, A126, A127, INTEGRA6:17;
A130: ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ c= dom F by A116, Lm1;
A131: for t being Real st t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ holds
( F is_differentiable_in t & diff (F,t) = (y (#) (x `| (dom x))) . t )

proof

let t be Real; :: thesis:
assume A132: t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ ; :: thesis:
then t in ].a1,b1.[ by A0, A106;
then y (#) (x `| (dom x)) is_continuous_in t by A2, A119, A121;
hence ( F is_differentiable_in t & diff (F,t) = (y (#) (x `| (dom x))) . t ) by A106, A117, A122, A123, A130, A132, INTEGRA6:28; :: thesis:

end;

A135: L . a < L . b by A1, A16, A9, A94;
then A136: ['(L . a),(L . b)'] = [.(L . a),(L . b).] by INTEGRA5:def 3;
A149: a1 + ((a - a1) / 2) in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A106;
A151: b1 - ((b1 - b) / 2) in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A106;
A137: ['(L . a),(L . b)'] c= ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A138: z in ['(L . a),(L . b)'] ; :: thesis:
then reconsider t = z as Real ;
A139: ( L . a <= t & t <= L . b ) by A136, A138, XXREAL_1:1;
( L . (a1 + ((a - a1) / 2)) < L . a & L . b < L . (b1 - ((b1 - b) / 2)) ) by A2, A5, A16, A106, A9, A149, A151;
then ( L . (a1 + ((a - a1) / 2)) < t & t < L . (b1 - ((b1 - b) / 2)) ) by A139, XXREAL_0:2;
hence z in ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ ; :: thesis:

end;

set G = F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[);
A143: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] c= dom L by A2, A106, RELAT_1:62;
for s being object holds
( s in L .: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] iff s in [.(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).] )

proof

let s be object ; :: thesis:

hereby :: thesis:

assume s in L .: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] ; :: thesis:
then consider x being object such that
A141: ( x in dom L & x in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] & s = L . x ) by FUNCT_1:def 6;
reconsider t = x as Real by A141;
A142: ( a1 + ((a - a1) / 2) <= t & t <= b1 - ((b1 - b) / 2) ) by A141, XXREAL_1:1;
A145: L . (a1 + ((a - a1) / 2)) <= L . t

proof

per cases ;

suppose a1 + ((a - a1) / 2) = t ; :: thesis:

hence L . (a1 + ((a - a1) / 2)) <= L . t ; :: thesis:

end;

suppose a1 + ((a - a1) / 2) <> t ; :: thesis:

then a1 + ((a - a1) / 2) < t by A142, XXREAL_0:1;
hence L . (a1 + ((a - a1) / 2)) <= L . t by A16, A141, A143, A149; :: thesis:

end;

L . t <= L . (b1 - ((b1 - b) / 2))

proof

per cases ;

suppose b1 - ((b1 - b) / 2) = t ; :: thesis:

hence L . t <= L . (b1 - ((b1 - b) / 2)) ; :: thesis:

end;

suppose b1 - ((b1 - b) / 2) <> t ; :: thesis:

then t < b1 - ((b1 - b) / 2) by A142, XXREAL_0:1;
hence L . t <= L . (b1 - ((b1 - b) / 2)) by A16, A141, A143, A151; :: thesis:

end;

hence s in [.(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).] by A141, A145; :: thesis:

end;

assume A147: s in [.(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).] ; :: thesis:
then reconsider t = s as Real ;

per cases by A147, XXREAL_1:1;

suppose L . (a1 + ((a - a1) / 2)) = t ; :: thesis:

hence s in L .: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A143, A149, FUNCT_1:def 6; :: thesis:

end;

suppose ( L . (a1 + ((a - a1) / 2)) <> t & L . (a1 + ((a - a1) / 2)) <= t & t <= L . (b1 - ((b1 - b) / 2)) & L . (b1 - ((b1 - b) / 2)) <> t ) ; :: thesis:

then A154: ( L . (a1 + ((a - a1) / 2)) < t & t < L . (b1 - ((b1 - b) / 2)) ) by XXREAL_0:1;
L | ].a1,b1.[ is continuous by A2, FDIFF_1:25;
then L | [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] is continuous ;
then consider u being Real such that
A155: ( a1 + ((a - a1) / 2) < u & u < b1 - ((b1 - b) / 2) & t = L . u ) by A106, A143, A154, Th1;
u in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A155;
hence s in L .: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A143, A155, FUNCT_1:def 6; :: thesis:

end;

suppose L . (b1 - ((b1 - b) / 2)) = t ; :: thesis:

hence s in L .: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A143, A151, FUNCT_1:def 6; :: thesis:

end;

then A157: L .: [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] = [.(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).] ;
Z1: ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ c= [.(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).] by Lm1;
A158: ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ c= rng L

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ ; :: thesis:
then consider t being object such that
A160: ( t in dom L & t in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] & z = L . t ) by Z1, A157, FUNCT_1:def 6;
thus z in rng L by A160, FUNCT_1:3; :: thesis:

end;

then A161: ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ c= dom (L ") by FUNCT_1:33;
then A162: dom ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) = ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ by RELAT_1:62;
rng ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) c= dom F

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) ; :: thesis:
then consider t being object such that
A163: ( t in dom ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) & z = ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t ) by FUNCT_1:def 3;
A165: z = (L ") . t by A162, A163, FUNCT_1:49;
consider s being object such that
A166: ( s in dom L & s in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] & t = L . s ) by Z1, A157, A162, A163, FUNCT_1:def 6;
thus z in dom F by A116, A165, A166, FUNCT_1:34; :: thesis:

end;

then A167: ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ = dom (F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) by A162, RELAT_1:27;
A168: for t being Real st t in ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ holds
( F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) is_differentiable_in t & ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ & diff ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)),t) = (diff (F,(((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t))) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t)) )

proof

let t be Real; :: thesis:
assume A169: t in ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ ; :: thesis:
then L " is_differentiable_in t by A27, A28, A158;
then A171: (L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ is_differentiable_in t by A161, A169, PDLAX:10;
A172: ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t = (L ") . t by A169, FUNCT_1:49;
consider s being object such that
A173: ( s in dom L & s in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] & t = L . s ) by Z1, A157, A169, FUNCT_1:def 6;
reconsider s = s as Real by A173;
(L ") . t in [.(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).] by A173, FUNCT_1:34;
then A174: ( a1 + ((a - a1) / 2) <= (L ") . t & (L ") . t <= b1 - ((b1 - b) / 2) ) by XXREAL_1:1;
A175: ( L . (a1 + ((a - a1) / 2)) < t & t < L . (b1 - ((b1 - b) / 2)) ) by A169, XXREAL_1:4;
( a1 + ((a - a1) / 2) <> (L ") . t & b1 - ((b1 - b) / 2) <> (L ") . t )

proof

assume ( not a1 + ((a - a1) / 2) <> (L ") . t or not b1 - ((b1 - b) / 2) <> (L ") . t ) ; :: thesis:

per cases ;

suppose a1 + ((a - a1) / 2) = (L ") . t ; :: thesis:

hence contradiction by A158, A169, A175, FUNCT_1:35; :: thesis:

end;

suppose b1 - ((b1 - b) / 2) = (L ") . t ; :: thesis:

hence contradiction by A158, A169, A175, FUNCT_1:35; :: thesis:

end;

then A178: ( a1 + ((a - a1) / 2) < (L ") . t & (L ") . t < b1 - ((b1 - b) / 2) ) by A174, XXREAL_0:1;
then (L ") . t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ ;
then F is_differentiable_in ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t by A131, A172;
hence ( F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) is_differentiable_in t & ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ & diff ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)),t) = (diff (F,(((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t))) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t)) ) by A171, A172, A178, FDIFF_2:13; :: thesis:

end;

then A179: F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) is_differentiable_on ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ by A167;
then A180: dom ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) = ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ by FDIFF_1:def 7;
dom ((x * (L ")) `| (dom (x * (L ")))) = dom (L ") by A47, A49, FDIFF_1:def 7;
then dom ((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) = (dom (L ")) /\ (dom (L ")) by A47, VALUED_1:def 4
.= dom (L ") ;
then A182: dom (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) = ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ by A161, RELAT_1:62;
for s being object st s in dom ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) holds
((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . s = (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . s

proof

let s be object ; :: thesis:
assume A183: s in dom ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) ; :: thesis:
then reconsider t = s as Real ;
(L ") . t in rng (L ") by A161, A180, A183, FUNCT_1:3;
then A186: (L ") . t in dom L by FUNCT_1:33;
set K = (L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[;
A189: ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t in ].(a1 + ((a - a1) / 2)),(b1 - ((b1 - b) / 2)).[ by A168, A180, A183;
A190: ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t = (L ") . t by A180, A183, FUNCT_1:49;
thus ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . s = diff ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)),t) by A179, A180, A183, FDIFF_1:def 7
.= (diff (F,(((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t))) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t)) by A168, A180, A183
.= ((y (#) (x `| (dom x))) . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t)) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t)) by A131, A189
.= ((y . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t)) * ((x `| (dom x)) . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t))) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t)) by VALUED_1:5
.= (y . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t)) * (((x `| (dom x)) . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . t)) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t)))
.= ((y * (L ")) . t) * (((x `| (dom x)) . ((L ") . t)) * (diff (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),t))) by A161, A180, A183, A190, FUNCT_1:13
.= ((y * (L ")) . t) * (((x `| (dom x)) . ((L ") . t)) * (diff ((L "),t))) by A27, A28, A158, A180, A183, PDLAX:11
.= ((y * (L ")) . t) * ((diff (x,((L ") . t))) * (diff ((L "),t))) by A1, A5, A45, A186, FDIFF_1:def 7
.= ((y * (L ")) . t) * (diff ((x * (L ")),t)) by A30, A158, A180, A183
.= ((y * (L ")) . t) * (((x * (L ")) `| (dom (x * (L ")))) . t) by A47, A49, A161, A180, A183, FDIFF_1:def 7
.= ((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) . t by VALUED_1:5
.= (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . s by A180, A183, FUNCT_1:49 ; :: thesis:

end;

then A192: ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) | ['(L . a),(L . b)'] = (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) | ['(L . a),(L . b)'] by A180, A182, FUNCT_1:2
.= ((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))) | ['(L . a),(L . b)'] by A137, RELAT_1:74 ;
A193: ['(L . a),(L . b)'] c= dom ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) by A137, A179, FDIFF_1:def 7;
(y * (L ")) | (dom (y * (L "))) is continuous by A51, FDIFF_1:25;
then ( ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) | ['(L . a),(L . b)'] is bounded & (F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[ is_integrable_on ['(L . a),(L . b)'] ) by A85, A192, A193, INTEGRA5:10, INTEGRA5:11;
then A194: (F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) . (L . b) = (integral (((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),(L . a),(L . b))) + ((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) . (L . a)) by A135, A137, A179, INTEGRA7:10;
A195: integral (((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),(L . a),(L . b)) = integral (((F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) `| ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[),['(L . a),(L . b)']) by A135, INTEGRA5:def 4
.= integral (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))),['(L . a),(L . b)']) by A192
.= integral (((y * (L ")) (#) ((x * (L ")) `| (dom (x * (L "))))),(L . a),(L . b)) by A135, INTEGRA5:def 4 ;
A196: ( L . a in [.(L . a),(L . b).] & L . b in [.(L . a),(L . b).] ) by A135;
then A197: (F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) . (L . a) = F . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . (L . a)) by A136, A137, A162, FUNCT_1:13
.= F . ((L ") . (L . a)) by A136, A137, A196, FUNCT_1:49
.= F . a by A9, A94, FUNCT_1:34 ;
A198: (F * ((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[)) . (L . b) = F . (((L ") | ].(L . (a1 + ((a - a1) / 2))),(L . (b1 - ((b1 - b) / 2))).[) . (L . b)) by A136, A137, A162, A196, FUNCT_1:13
.= F . ((L ") . (L . b)) by A136, A137, A196, FUNCT_1:49
.= F . b by A9, A94, FUNCT_1:34 ;
A200: [.(L . a),(L . b).] c= dom (L ") by A136, A137, A161;
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

proof

let s be Real; :: thesis:
assume s in (dom (x * (L "))) /\ (dom (y * (L "))) ; :: thesis:
then s in rng L by A47, FUNCT_1:33;
hence ((diff ((x * (L ")),s)) ^2) + ((diff ((y * (L ")),s)) ^2) = 1 by A30; :: thesis:

end;

hence ( 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 A1, A2, A6, A10, A16, A19, A20, A23, A30, A43, A45, A49, A51, A57, A58, A59, A60, A61, A62, A69, A70, A71, A84, A86, A104, A124, A129, A194, A195, A197, A198, A200, FDIFF_2:48, FUNCT_1:2, FUNCT_1:33, RELAT_1:27; :: thesis: