let x, y be PartFunc of REAL,REAL; :: thesis:
let a, b be 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
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = 1 ) & y . a = 0 & y . b = 0 ) ; :: thesis:
set K = (b - a) / PI;
A3: 0 < b - a by A1, XREAL_1:50;
A4: ( dom (x `| (dom x)) = dom x & dom (y `| (dom y)) = dom y ) by A1, FDIFF_1:def 7;
A5: ['0,PI'] = [.0,PI.] by COMPTRIG:5, INTEGRA5:def 3;
A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
PI + 0 < PI + 1 by XREAL_1:8;
then A7: [.0,PI.] c= ].(- 1),(PI + 1).[ by XXREAL_1:47;
set G = PI / (b - a);
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 ;
consider a1, b1 being Real such that
A10: ( a1 < a & b < b1 & a1 < b1 & [.a1,b1.] c= Z & [.a,b.] c= ].a1,b1.[ ) by A1, A6, Th2, XBOOLE_1:19;
set T = AffineMap (((b - a) / PI),a);
A11: for t being Real holds (AffineMap (((b - a) / PI),a)) . t = (((b - a) / PI) * t) + a by FCONT_1:def 4;
A13: dom (AffineMap (((b - a) / PI),a)) = [#] REAL by FUNCT_2:def 1;
A14: for t being Real st t in REAL holds
(AffineMap (((b - a) / PI),a)) . t = (((b - a) / PI) * t) + a by FCONT_1:def 4;
then A21: ( AffineMap (((b - a) / PI),a) is_differentiable_on REAL & ( for t being Real st t in REAL holds
((AffineMap (((b - a) / PI),a)) `| REAL) . t = (b - a) / PI ) ) by A13, FDIFF_1:23;
A23: AffineMap (((b - a) / PI),a) is_differentiable_on ].(- 1),(PI + 1).[ by A13, A14, FDIFF_1:23, FDIFF_1:26;

let t1, t2 be object ; :: thesis:
assume A24: ( t1 in dom (AffineMap (((b - a) / PI),a)) & t2 in dom (AffineMap (((b - a) / PI),a)) & (AffineMap (((b - a) / PI),a)) . t1 = (AffineMap (((b - a) / PI),a)) . t2 ) ; :: thesis:
then reconsider s1 = t1, s2 = t2 as Real ;
(((b - a) / PI) * s1) + a = (AffineMap (((b - a) / PI),a)) . s2 by FCONT_1:def 4, A24
.= (((b - a) / PI) * s2) + a by FCONT_1:def 4 ;
then s1 = (((b - a) / PI) * s2) / ((b - a) / PI) by A3, COMPTRIG:5, XCMPLX_1:89
.= s2 by A3, COMPTRIG:5, XCMPLX_1:89 ;
hence t1 = t2 ; :: thesis:

end;

then reconsider T = AffineMap (((b - a) / PI),a) as one-to-one PartFunc of REAL,REAL by FUNCT_1:def 4;

now :: thesis:

let t be Real; :: thesis:
assume A25: t in ].(- 1),(PI + 1).[ ; :: thesis:
then (T `| REAL) . t = (b - a) / PI by A13, A14, FDIFF_1:23;
hence 0 < diff (T,t) by A3, A21, A25, FDIFF_1:def 7, COMPTRIG:5; :: thesis:

end;

then A26: T | ].(- 1),(PI + 1).[ is increasing by A23, ROLLE:9;
A27: dom (T | ].(- 1),(PI + 1).[) = ].(- 1),(PI + 1).[ by A13, RELAT_1:62;
A28: ( x is_differentiable_on dom x & y is_differentiable_on dom y ) by A1;
A29: ( dom x is open & dom y is open ) by A1, FDIFF_1:10;
then reconsider DX = T " (dom x) as open Subset of REAL by A13, Lm2;
reconsider DY = T " (dom y) as open Subset of REAL by A13, A29, Lm2;
set x1 = (PI / (b - a)) (#) (x * T);
set y1 = (PI / (b - a)) (#) (y * T);
A30: dom (x * T) = DX by RELAT_1:147;
then A32: dom ((PI / (b - a)) (#) (x * T)) = DX by VALUED_1:def 5;
A31: dom (y * T) = DY by RELAT_1:147;
then A33: dom ((PI / (b - a)) (#) (y * T)) = DY by VALUED_1:def 5;
A34: for t being Real holds
( t in DX iff T . t in dom x )

proof

let t be Real; :: thesis:
thus ( t in DX implies T . t in dom x ) by FUNCT_1:def 7; :: thesis:
assume A35: T . t in dom x ; :: thesis:
t in dom T by A13, XREAL_0:def 1;
hence t in DX by A35, FUNCT_1:def 7; :: thesis:

end;

A39: rng (T | DX) c= dom x

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in rng (T | DX) ; :: thesis:
then consider s being object such that
A36: ( s in dom (T | DX) & t = (T | DX) . s ) by FUNCT_1:def 3;
A37: dom (T | DX) = (dom T) /\ DX by RELAT_1:61;
reconsider s = s as Real by A36;
( s in dom T & t = T . s ) by A36, A37, FUNCT_1:49, XBOOLE_0:def 4;
hence t in dom x by A34, A36; :: thesis:

end;

A46: for t being Real holds
( t in DY iff T . t in dom y )

proof

let t be Real; :: thesis:
thus ( t in DY implies T . t in dom y ) by FUNCT_1:def 7; :: thesis:
assume A47: T . t in dom y ; :: thesis:
t in dom T by A13, XREAL_0:def 1;
hence t in DY by A47, FUNCT_1:def 7; :: thesis:

end;

A51: rng (T | DY) c= dom y

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in rng (T | DY) ; :: thesis:
then consider s being object such that
A48: ( s in dom (T | DY) & t = (T | DY) . s ) by FUNCT_1:def 3;
A49: dom (T | DY) = (dom T) /\ DY by RELAT_1:61;
reconsider s = s as Real by A48;
( s in dom T & t = T . s ) by A48, A49, XBOOLE_0:def 4, FUNCT_1:49;
hence t in dom y by A46, A48; :: thesis:

end;

dom y c= rng (T | DY)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A52: t in dom y ; :: thesis:
then reconsider u = t as Real ;
set s = (u - a) / ((b - a) / PI);
A53: T . ((u - a) / ((b - a) / PI)) = (((b - a) / PI) * ((u - a) / ((b - a) / PI))) + a by FCONT_1:def 4
.= (u - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= t ;
(u - a) / ((b - a) / PI) in dom T by A13, XREAL_0:def 1;
then A55: (u - a) / ((b - a) / PI) in DY by A52, A53, FUNCT_1:def 7;
then A56: t = (T | DY) . ((u - a) / ((b - a) / PI)) by A53, FUNCT_1:49;
(u - a) / ((b - a) / PI) in dom (T | DY) by A13, A55, RELAT_1:57;
hence t in rng (T | DY) by A56, FUNCT_1:3; :: thesis:

end;

then A57: rng (T | DY) = dom y by A51;
A58: for t being Real st t in DX holds
( (PI / (b - a)) (#) (x * T) is_differentiable_in t & diff (((PI / (b - a)) (#) (x * T)),t) = diff (x,(T . t)) )

proof

let t be Real; :: thesis:
assume A59: t in DX ; :: thesis:
A60: t in REAL by XREAL_0:def 1;
A61: T is_differentiable_in t by A21, XREAL_0:def 1;
x is_differentiable_in T . t by A28, A34, A59;
then A62: ( x * T is_differentiable_in t & diff ((x * T),t) = (diff (x,(T . t))) * (diff (T,t)) ) by A61, FDIFF_2:13;
then A63: ( (PI / (b - a)) (#) (x * T) is_differentiable_in t & diff (((PI / (b - a)) (#) (x * T)),t) = (PI / (b - a)) * (diff ((x * T),t)) ) by FDIFF_1:15;
(T `| REAL) . t = (b - a) / PI by A13, A14, FDIFF_1:23, XREAL_0:def 1;
then diff (T,t) = (b - a) / PI by A21, A60, FDIFF_1:def 7;
then diff (((PI / (b - a)) (#) (x * T)),t) = ((PI / (b - a)) * ((b - a) / PI)) * (diff (x,(T . t))) by A62, A63
.= 1 * (diff (x,(T . t))) by A3, COMPTRIG:5, XCMPLX_1:112 ;
hence ( (PI / (b - a)) (#) (x * T) is_differentiable_in t & diff (((PI / (b - a)) (#) (x * T)),t) = diff (x,(T . t)) ) by A62, FDIFF_1:15; :: thesis:

end;

then A64: (PI / (b - a)) (#) (x * T) is_differentiable_on DX by A32;
then A65: (PI / (b - a)) (#) (x * T) is differentiable by A30, VALUED_1:def 5;
A66: dom (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) = DX by A32, A64, FDIFF_1:def 7;
A67: dom ((x `| (dom x)) * (T | DX)) = dom (T | DX) by A4, A39, RELAT_1:27
.= DX by A13, RELAT_1:62 ;
for t being object st t in dom (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) holds
(((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) . t = ((x `| (dom x)) * (T | DX)) . t

proof

let t be object ; :: thesis:
assume A68: t in dom (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) ; :: thesis:
then reconsider s = t as Real ;
A70: T . s in dom x by A34, A66, A68;
t in dom ((PI / (b - a)) (#) (x * T)) by A65, A68, FDIFF_1:def 7;
hence (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) . t = diff (((PI / (b - a)) (#) (x * T)),s) by A65, FDIFF_1:def 7
.= diff (x,(T . s)) by A58, A66, A68
.= (x `| (dom x)) . (T . s) by A1, A70, FDIFF_1:def 7
.= (x `| (dom x)) . ((T | DX) . s) by A66, A68, FUNCT_1:49
.= ((x `| (dom x)) * (T | DX)) . t by A66, A67, A68, FUNCT_1:12 ;
:: thesis:

end;

then A72: ((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))) is continuous by A1, A66, A67, FUNCT_1:2;
A73: for t being Real st t in DY holds
( (PI / (b - a)) (#) (y * T) is_differentiable_in t & diff (((PI / (b - a)) (#) (y * T)),t) = diff (y,(T . t)) )

proof

let t be Real; :: thesis:
assume A74: t in DY ; :: thesis:
A75: t in REAL by XREAL_0:def 1;
A76: T is_differentiable_in t by A21, XREAL_0:def 1;
y is_differentiable_in T . t by A28, A46, A74;
then A77: ( y * T is_differentiable_in t & diff ((y * T),t) = (diff (y,(T . t))) * (diff (T,t)) ) by A76, FDIFF_2:13;
then A78: ( (PI / (b - a)) (#) (y * T) is_differentiable_in t & diff (((PI / (b - a)) (#) (y * T)),t) = (PI / (b - a)) * (diff ((y * T),t)) ) by FDIFF_1:15;
(T `| REAL) . t = (b - a) / PI by A13, A14, FDIFF_1:23, XREAL_0:def 1;
then diff (T,t) = (b - a) / PI by A21, A75, FDIFF_1:def 7;
then diff (((PI / (b - a)) (#) (y * T)),t) = ((PI / (b - a)) * ((b - a) / PI)) * (diff (y,(T . t))) by A77, A78
.= 1 * (diff (y,(T . t))) by A3, COMPTRIG:5, XCMPLX_1:112 ;
hence ( (PI / (b - a)) (#) (y * T) is_differentiable_in t & diff (((PI / (b - a)) (#) (y * T)),t) = diff (y,(T . t)) ) by A77, FDIFF_1:15; :: thesis:

end;

then B79: (PI / (b - a)) (#) (y * T) is_differentiable_on DY by A33;
then A80: (PI / (b - a)) (#) (y * T) is differentiable by A31, VALUED_1:def 5;
A81: dom (((PI / (b - a)) (#) (y * T)) `| (dom ((PI / (b - a)) (#) (y * T)))) = DY by A33, B79, FDIFF_1:def 7;
A82: dom ((y `| (dom y)) * (T | DY)) = dom (T | DY) by A4, A57, RELAT_1:27
.= DY by A13, RELAT_1:62 ;
A92: ( 0 in [.0,PI.] & PI in [.0,PI.] ) by COMPTRIG:5;
for t being object st t in dom (((PI / (b - a)) (#) (y * T)) `| (dom ((PI / (b - a)) (#) (y * T)))) holds
(((PI / (b - a)) (#) (y * T)) `| (dom ((PI / (b - a)) (#) (y * T)))) . t = ((y `| (dom y)) * (T | DY)) . t

proof

let t be object ; :: thesis:
assume A83: t in dom (((PI / (b - a)) (#) (y * T)) `| (dom ((PI / (b - a)) (#) (y * T)))) ; :: thesis:
then reconsider s = t as Real ;
A85: T . s in dom y by A46, A81, A83;
t in dom ((PI / (b - a)) (#) (y * T)) by A80, A83, FDIFF_1:def 7;
hence (((PI / (b - a)) (#) (y * T)) `| (dom ((PI / (b - a)) (#) (y * T)))) . t = diff (((PI / (b - a)) (#) (y * T)),s) by A80, FDIFF_1:def 7
.= diff (y,(T . s)) by A73, A81, A83
.= (y `| (dom y)) . (T . s) by A1, A85, FDIFF_1:def 7
.= (y `| (dom y)) . ((T | DY) . s) by A81, A83, FUNCT_1:49
.= ((y `| (dom y)) * (T | DY)) . t by A81, A82, A83, FUNCT_1:12 ;
:: thesis:

end;

then A87: ((PI / (b - a)) (#) (y * T)) `| (dom ((PI / (b - a)) (#) (y * T))) is continuous by A1, A81, A82, FUNCT_1:2;
A95: T . PI = (((b - a) / PI) * PI) + a by FCONT_1:def 4
.= (b - a) + a by COMPTRIG:5, XCMPLX_1:87
.= b ;

A88: now :: thesis:

let t be object ; :: thesis:
assume A89: t in ['0,PI'] ; :: thesis:
then reconsider s = t as Real ;
A90: s in ].(- 1),(PI + 1).[ by A5, A7, A89;
set T1 = T | ].(- 1),(PI + 1).[;
A94: ( (T | ].(- 1),(PI + 1).[) . s = T . s & (T | ].(- 1),(PI + 1).[) . 0 = T . 0 & (T | ].(- 1),(PI + 1).[) . PI = T . PI ) by A5, A7, A89, A92, FUNCT_1:49;
( 0 <= s & s <= PI ) by A5, A89, XXREAL_1:1;
then ( ( 0 = s or 0 < s ) & ( s = PI or s < PI ) ) by XXREAL_0:1;
then ( (T | ].(- 1),(PI + 1).[) . 0 <= (T | ].(- 1),(PI + 1).[) . s & (T | ].(- 1),(PI + 1).[) . s <= (T | ].(- 1),(PI + 1).[) . PI ) by A26, A27, A90, A7, A92;
then ( (((b - a) / PI) * 0) + a <= T . s & T . s <= T . PI ) by FCONT_1:def 4, A94;
hence T . t in [.a,b.] by A95; :: thesis:

end;

A96: ['0,PI'] c= dom ((PI / (b - a)) (#) (x * T))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A97: t in ['0,PI'] ; :: thesis:
then reconsider s = t as Real ;
T . s in dom x by A1, A6, A88, A97;
hence t in dom ((PI / (b - a)) (#) (x * T)) by A32, A34; :: thesis:

end;

A99: ['0,PI'] c= dom ((PI / (b - a)) (#) (y * T))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A100: t in ['0,PI'] ; :: thesis:
then reconsider s = t as Real ;
T . s in dom y by A1, A6, A88, A100;
hence t in dom ((PI / (b - a)) (#) (y * T)) by A33, A46; :: thesis:

end;

A102: for t being Real st t in (dom ((PI / (b - a)) (#) (x * T))) /\ (dom ((PI / (b - a)) (#) (y * T))) holds
((diff (((PI / (b - a)) (#) (x * T)),t)) ^2) + ((diff (((PI / (b - a)) (#) (y * T)),t)) ^2) = 1

proof

let t be Real; :: thesis:
assume t in (dom ((PI / (b - a)) (#) (x * T))) /\ (dom ((PI / (b - a)) (#) (y * T))) ; :: thesis:
then A103: ( t in DX & t in DY ) by A32, A33, XBOOLE_0:def 4;
then ( T . t in dom x & T . t in dom y ) by A34, A46;
then A104: T . t in (dom x) /\ (dom y) by XBOOLE_0:def 4;
( diff (((PI / (b - a)) (#) (x * T)),t) = diff (x,(T . t)) & diff (((PI / (b - a)) (#) (y * T)),t) = diff (y,(T . t)) ) by A58, A73, A103;
hence ((diff (((PI / (b - a)) (#) (x * T)),t)) ^2) + ((diff (((PI / (b - a)) (#) (y * T)),t)) ^2) = 1 by A1, A104; :: thesis:

end;

A106: T . 0 = (((b - a) / PI) * 0) + a by FCONT_1:def 4
.= a ;
A110: ((PI / (b - a)) (#) (y * T)) . 0 = (PI / (b - a)) * ((y * T) . 0) by VALUED_1:6
.= (PI / (b - a)) * (y . (T . 0)) by A5, A31, A33, A92, A99, FUNCT_1:12
.= 0 by A1, A106 ;
A111: ((PI / (b - a)) (#) (y * T)) . PI = (PI / (b - a)) * ((y * T) . PI) by VALUED_1:6
.= (PI / (b - a)) * (y . (T . PI)) by A5, A31, A33, A92, A99, FUNCT_1:12
.= 0 by A1, A95 ;
A113: ((PI / (b - a)) (#) (x * T)) . 0 = (PI / (b - a)) * ((x * T) . 0) by VALUED_1:6
.= (PI / (b - a)) * (x . a) by A5, A30, A32, A92, A96, A106, FUNCT_1:12 ;
A114: ( integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI) <= (1 / 2) * PI & ( not integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( ((PI / (b - a)) (#) (y * T)) . t = sin . t & ((PI / (b - a)) (#) (x * T)) . t = ((- (cos . t)) + (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) or for t being Real st t in [.0,PI.] holds
( ((PI / (b - a)) (#) (y * T)) . t = - (sin . t) & ((PI / (b - a)) (#) (x * T)) . t = ((cos . t) - (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( ((PI / (b - a)) (#) (y * T)) . t = sin . t & ((PI / (b - a)) (#) (x * T)) . t = ((- (cos . t)) + (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) or for t being Real st t in [.0,PI.] holds
( ((PI / (b - a)) (#) (y * T)) . t = - (sin . t) & ((PI / (b - a)) (#) (x * T)) . t = ((cos . t) - (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) ) implies integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI) = (1 / 2) * PI ) ) by A65, A72, A80, A87, A96, A99, A102, A110, A111, PDLAX:16;
deffunc H₁( Real) -> Element of REAL = In ((integral ((y (#) (x `| (dom x))),a1,$1)),REAL);
consider S0 being Function of REAL,REAL such that
A115: for t being Element of REAL holds S0 . t = H₁(t) from FUNCT_2:sch 4();
A116: for t being Real holds S0 . t = integral ((y (#) (x `| (dom x))),a1,t)

proof

let t be Real; :: thesis:
t in REAL by XREAL_0:def 1;
then S0 . t = In ((integral ((y (#) (x `| (dom x))),a1,t)),REAL) by A115;
hence S0 . t = integral ((y (#) (x `| (dom x))),a1,t) ; :: thesis:

end;

set S = S0 | [.a1,b1.];
dom S0 = REAL by FUNCT_2:def 1;
then A117: dom (S0 | [.a1,b1.]) = [.a1,b1.] by RELAT_1:62;
C1: ].a1,b1.[ c= [.a1,b1.] by Lm1;
reconsider S = S0 | [.a1,b1.] as PartFunc of REAL,REAL ;
A118: for t being Real st t in ].a1,b1.[ holds
S . t = integral ((y (#) (x `| (dom x))),a1,t)

proof

let t be Real; :: thesis:
assume t in ].a1,b1.[ ; :: thesis:
hence S . t = S0 . t by C1, FUNCT_1:49
.= integral ((y (#) (x `| (dom x))),a1,t) by A116 ;
:: thesis:

end;

B119: y | (dom y) is continuous by A1, FDIFF_1:25;
then A120: y (#) (x `| (dom x)) is continuous by A1;
A121: (y (#) (x `| (dom x))) | ['a1,b1'] is continuous by A1, B119;
A122: dom (y (#) (x `| (dom x))) = (dom y) /\ (dom (x `| (dom x))) by VALUED_1:def 4
.= Z by A1, FDIFF_1:def 7 ;
A123: ['a1,b1'] c= dom (y (#) (x `| (dom x))) by A10, A122, INTEGRA5:def 3;
then A124: ( (y (#) (x `| (dom x))) | ['a1,b1'] is bounded & y (#) (x `| (dom x)) is_integrable_on ['a1,b1'] ) by A121, INTEGRA5:10, INTEGRA5:11;
B0: ( a in [.a,b.] & b in [.a,b.] ) by A1;
then A125: ( S . a = integral ((y (#) (x `| (dom x))),a1,a) & S . b = integral ((y (#) (x `| (dom x))),a1,b) ) by A10, A118;
A126: a1 < b by A1, A10, XXREAL_0:2;
A128: ['a1,b'] c= dom (y (#) (x `| (dom x)))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A127: z in ['a1,b'] ; :: thesis:
then reconsider t = z as Real ;
z in [.a1,b.] by A1, A10, A127, INTEGRA5:def 3, XXREAL_0:2;
then ( a1 <= t & t <= b ) by XXREAL_1:1;
then ( a1 <= t & t <= b1 ) by A10, XXREAL_0:2;
then t in [.a1,b1.] ;
then t in ['a1,b1'] by A10, INTEGRA5:def 3;
hence z in dom (y (#) (x `| (dom x))) by A123; :: thesis:

end;

(y (#) (x `| (dom x))) | ['a1,b'] is continuous by A1, B119;
then A129: ( (y (#) (x `| (dom x))) | ['a1,b'] is bounded & y (#) (x `| (dom x)) is_integrable_on ['a1,b'] ) by A128, INTEGRA5:10, INTEGRA5:11;
A130: ( a1 < a & a < b1 ) by B0, A10, XXREAL_1:4;
a in [.a1,b.] by A1, A10;
then a in ['a1,b'] by A1, A130, INTEGRA5:def 3, XXREAL_0:2;
then A131: integral ((y (#) (x `| (dom x))),a1,b) = (integral ((y (#) (x `| (dom x))),a1,a)) + (integral ((y (#) (x `| (dom x))),a,b)) by A126, A128, A129, INTEGRA6:17;
A132: ].a1,b1.[ c= dom S by A117, Lm1;
A133: for t being Real st t in ].a1,b1.[ holds
( S is_differentiable_in t & diff (S,t) = (y (#) (x `| (dom x))) . t )

proof

let t be Real; :: thesis:
assume A134: t in ].a1,b1.[ ; :: thesis:
then y (#) (x `| (dom x)) is_continuous_in t by A10, A120, A122, C1;
hence ( S is_differentiable_in t & diff (S,t) = (y (#) (x `| (dom x))) . t ) by A10, A118, A123, A124, A132, A134, INTEGRA6:28; :: thesis:

end;

set P1 = (a1 - a) / ((b - a) / PI);
set Q1 = (b1 - a) / ((b - a) / PI);
A136: ( (a1 - a) / ((b - a) / PI) < 0 & PI < (b1 - a) / ((b - a) / PI) & (a1 - a) / ((b - a) / PI) < (b1 - a) / ((b - a) / PI) )

proof

A138: a1 - a < 0 by A10, XREAL_1:49;
hence (a1 - a) / ((b - a) / PI) < 0 by A3, COMPTRIG:5; :: thesis:
A139: (b1 - a) / ((b - a) / PI) = PI * ((b1 - a) / (b - a)) by XCMPLX_1:81
.= PI * (((b - a) / (b - a)) + ((b1 - b) / (b - a)))
.= PI * (1 + ((b1 - b) / (b - a))) by A3, XCMPLX_1:60
.= PI + (PI * ((b1 - b) / (b - a))) ;
0 < b1 - b by A10, XREAL_1:50;
then PI + 0 < PI + (PI * ((b1 - b) / (b - a))) by A3, COMPTRIG:5, XREAL_1:8;
hence ( PI < (b1 - a) / ((b - a) / PI) & (a1 - a) / ((b - a) / PI) < (b1 - a) / ((b - a) / PI) ) by A3, A138, A139, COMPTRIG:5; :: thesis:

end;

A141: ( [.0,PI.] c= ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ & ['0,PI'] c= ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ & ['0,PI'] c= ['((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI))'] & [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] c= DX /\ DY )

proof

A142: [.0,PI.] c= ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ by A136, XXREAL_1:47;
thus ( [.0,PI.] c= ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ & ['0,PI'] c= ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ ) by A5, A136, XXREAL_1:47; :: thesis:
].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ c= [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] by Lm1;
then ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ c= ['((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI))'] by A136, INTEGRA5:def 3;
hence ['0,PI'] c= ['((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI))'] by A5, A142; :: thesis:
let s be object ; :: according to TARSKI:def 3 :: thesis:
assume A148: s in [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] ; :: thesis:
then reconsider t = s as Real ;
A149: ( (a1 - a) / ((b - a) / PI) <= t & t <= (b1 - a) / ((b - a) / PI) ) by A148, XXREAL_1:1;
A150: ( T . t = (((b - a) / PI) * t) + a & T . ((a1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a & T . ((b1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by FCONT_1:def 4;
then A151: T . ((a1 - a) / ((b - a) / PI)) = (a1 - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= a1 ;
A152: T . ((b1 - a) / ((b - a) / PI)) = (b1 - a) + a by A3, A150, COMPTRIG:5, XCMPLX_1:87
.= b1 ;
( ((b - a) / PI) * ((a1 - a) / ((b - a) / PI)) <= ((b - a) / PI) * t & ((b - a) / PI) * t <= ((b - a) / PI) * ((b1 - a) / ((b - a) / PI)) ) by A3, A149, COMPTRIG:5, XREAL_1:64;
then ( (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a <= (((b - a) / PI) * t) + a & (((b - a) / PI) * t) + a <= (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by XREAL_1:7;
then T . t in [.a1,b1.] by A150, A151, A152;
then ( T . t in dom x & T . t in dom y ) by A10, XBOOLE_0:def 4;
then ( s in DX & s in DY ) by A34, A46;
hence s in DX /\ DY by XBOOLE_0:def 4; :: thesis:

end;

BB: ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ c= [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] by Lm1;
then B142: ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ c= DX /\ DY by A141;
set W = S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[);
A155: dom (((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) = DY /\ DX by A33, A66, VALUED_1:def 4;
A157: for s being Real holds
( T . s in [.a1,b1.] iff s in [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] )

proof

let s be Real; :: thesis:

hereby :: thesis:

assume T . s in [.a1,b1.] ; :: thesis:
then A158: ( a1 <= T . s & T . s <= b1 ) by XXREAL_1:1;
A159: ( T . s = (((b - a) / PI) * s) + a & T . ((a1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a & T . ((b1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by FCONT_1:def 4;
then A160: T . ((a1 - a) / ((b - a) / PI)) = (a1 - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= a1 ;
T . ((b1 - a) / ((b - a) / PI)) = (b1 - a) + a by A3, A159, COMPTRIG:5, XCMPLX_1:87
.= b1 ;
then ( ((((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a) - a <= ((((b - a) / PI) * s) + a) - a & ((((b - a) / PI) * s) + a) - a <= ((((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a) - a ) by A158, A159, A160, XREAL_1:13;
then A162: ( (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) / ((b - a) / PI) <= (((b - a) / PI) * s) / ((b - a) / PI) & (((b - a) / PI) * s) / ((b - a) / PI) <= (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) / ((b - a) / PI) ) by A3, COMPTRIG:5, XREAL_1:72;
then (a1 - a) / ((b - a) / PI) <= (((b - a) / PI) * s) / ((b - a) / PI) by A3, COMPTRIG:5, XCMPLX_1:89;
then A163: (a1 - a) / ((b - a) / PI) <= s by A3, COMPTRIG:5, XCMPLX_1:89;
s <= (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) / ((b - a) / PI) by A3, A162, COMPTRIG:5, XCMPLX_1:89;
then s <= (b1 - a) / ((b - a) / PI) by A3, COMPTRIG:5, XCMPLX_1:89;
hence s in [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] by A163; :: thesis:

end;

assume s in [.((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).] ; :: thesis:
then A165: ( (a1 - a) / ((b - a) / PI) <= s & s <= (b1 - a) / ((b - a) / PI) ) by XXREAL_1:1;
A166: ( T . s = (((b - a) / PI) * s) + a & T . ((a1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a & T . ((b1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by FCONT_1:def 4;
then A167: T . ((a1 - a) / ((b - a) / PI)) = (a1 - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= a1 ;
A168: T . ((b1 - a) / ((b - a) / PI)) = (b1 - a) + a by A3, A166, COMPTRIG:5, XCMPLX_1:87
.= b1 ;
( ((b - a) / PI) * ((a1 - a) / ((b - a) / PI)) <= ((b - a) / PI) * s & ((b - a) / PI) * s <= ((b - a) / PI) * ((b1 - a) / ((b - a) / PI)) ) by A3, A165, COMPTRIG:5, XREAL_1:64;
then ( (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a <= (((b - a) / PI) * s) + a & (((b - a) / PI) * s) + a <= (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by XREAL_1:7;
hence T . s in [.a1,b1.] by A166, A167, A168; :: thesis:

end;

A169: for s being Real holds
( T . s in ].a1,b1.[ iff s in ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ )

proof

let s be Real; :: thesis:
A171: ( T . s = (((b - a) / PI) * s) + a & T . ((a1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a & T . ((b1 - a) / ((b - a) / PI)) = (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by FCONT_1:def 4;
then A172: T . ((a1 - a) / ((b - a) / PI)) = (a1 - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= a1 ;
B1: T . ((b1 - a) / ((b - a) / PI)) = (b1 - a) + a by A3, A171, COMPTRIG:5, XCMPLX_1:87
.= b1 ;

hereby :: thesis:

assume T . s in ].a1,b1.[ ; :: thesis:
then ( a1 < T . s & T . s < b1 ) by XXREAL_1:4;
then ( ((((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a) - a < ((((b - a) / PI) * s) + a) - a & ((((b - a) / PI) * s) + a) - a < ((((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a) - a ) by A171, A172, B1, XREAL_1:14;
then A174: ( (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) / ((b - a) / PI) < (((b - a) / PI) * s) / ((b - a) / PI) & (((b - a) / PI) * s) / ((b - a) / PI) < (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) / ((b - a) / PI) ) by A3, COMPTRIG:5, XREAL_1:74;
then (a1 - a) / ((b - a) / PI) < (((b - a) / PI) * s) / ((b - a) / PI) by A3, COMPTRIG:5, XCMPLX_1:89;
then A175: (a1 - a) / ((b - a) / PI) < s by A3, COMPTRIG:5, XCMPLX_1:89;
s < (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) / ((b - a) / PI) by A3, A174, COMPTRIG:5, XCMPLX_1:89;
then s < (b1 - a) / ((b - a) / PI) by A3, COMPTRIG:5, XCMPLX_1:89;
hence s in ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ by A175; :: thesis:

end;

assume s in ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ ; :: thesis:
then ( (a1 - a) / ((b - a) / PI) < s & s < (b1 - a) / ((b - a) / PI) ) by XXREAL_1:4;
then ( ((b - a) / PI) * ((a1 - a) / ((b - a) / PI)) < ((b - a) / PI) * s & ((b - a) / PI) * s < ((b - a) / PI) * ((b1 - a) / ((b - a) / PI)) ) by A3, COMPTRIG:5, XREAL_1:68;
then ( (((b - a) / PI) * ((a1 - a) / ((b - a) / PI))) + a < (((b - a) / PI) * s) + a & (((b - a) / PI) * s) + a < (((b - a) / PI) * ((b1 - a) / ((b - a) / PI))) + a ) by XREAL_1:8;
hence T . s in ].a1,b1.[ by A171, A172, B1; :: thesis:

end;

A181: dom (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) = ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ by A13, RELAT_1:62;

now :: thesis:

let z be object ; :: thesis:
assume z in rng (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) ; :: thesis:
then consider t being object such that
A182: ( t in dom (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) & z = (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t ) by FUNCT_1:def 3;
z = T . t by A181, A182, FUNCT_1:49;
hence z in dom S by BB, A117, A157, A181, A182; :: thesis:

end;

then rng (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) c= dom S ;
then A185: ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ = dom (S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) by A181, RELAT_1:27;
A186: for t being Real st t in ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ holds
( S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) is_differentiable_in t & (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t in ].a1,b1.[ & diff ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)),t) = (diff (S,((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t))) * (diff ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),t)) )

proof

let t be Real; :: thesis:
assume A187: t in ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ ; :: thesis:
then T is_differentiable_in t by A21;
then A188: T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ is_differentiable_in t by A13, A187, PDLAX:10;
A189: (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t = T . t by A187, FUNCT_1:49;
then (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t in ].a1,b1.[ by A169, A187;
then S is_differentiable_in (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t by A133;
hence ( S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) is_differentiable_in t & (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t in ].a1,b1.[ & diff ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)),t) = (diff (S,((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t))) * (diff ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),t)) ) by A169, A187, A188, A189, FDIFF_2:13; :: thesis:

end;

then A191: S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) is_differentiable_on ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ by A185;
then A192: dom ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) = ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ by FDIFF_1:def 7;
A193: dom ((((b - a) / PI) ^2) (#) ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) = dom ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) by VALUED_1:def 5
.= ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ by B142, A155, RELAT_1:62 ;
for s being object st s in dom ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) holds
((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . s = ((((b - a) / PI) ^2) (#) ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) . s

proof

let s be object ; :: thesis:
assume A194: s in dom ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) ; :: thesis:
then reconsider t = s as Real ;
T . t in [.a1,b1.] by A169, A192, A194, C1;
then A196: ( T . t in dom x & T . t in dom y ) by A10, XBOOLE_0:def 4;
then A197: t in dom ((PI / (b - a)) (#) (x * T)) by A32, A34;
A198: t in REAL by XREAL_0:def 1;
(T `| REAL) . t = (b - a) / PI by A13, A14, FDIFF_1:23, XREAL_0:def 1;
then A201: diff (T,t) = (b - a) / PI by A21, A198, FDIFF_1:def 7;
set L = T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[;
A202: (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t in ].a1,b1.[ by A186, A192, A194;
A203: (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t = T . t by A192, A194, FUNCT_1:49;
((PI / (b - a)) (#) (y * T)) . t = (PI / (b - a)) * ((y * T) . t) by VALUED_1:6
.= (PI / (b - a)) * (y . (T . t)) by A13, FUNCT_1:13, XREAL_0:def 1 ;
then A205: ((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t) = (((b - a) / PI) * (PI / (b - a))) * (y . (T . t))
.= 1 * (y . (T . t)) by A3, COMPTRIG:5, XCMPLX_1:112 ;
thus ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . s = diff ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)),t) by A191, A192, A194, FDIFF_1:def 7
.= (diff (S,((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t))) * (diff ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),t)) by A186, A192, A194
.= ((y (#) (x `| (dom x))) . ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t)) * (diff ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),t)) by A133, A202
.= ((y . ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t)) * ((x `| (dom x)) . ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t))) * (diff ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),t)) by VALUED_1:5
.= (((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t)) * (((x `| (dom x)) . ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t)) * (diff ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),t))) by A203, A205
.= (((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t)) * (((x `| (dom x)) . (T . t)) * (diff (T,t))) by A13, A21, A192, A194, A203, PDLAX:11
.= (((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t)) * ((diff (x,(T . t))) * ((b - a) / PI)) by A1, A196, A201, FDIFF_1:def 7
.= ((((b - a) / PI) ^2) * (((PI / (b - a)) (#) (y * T)) . t)) * (diff (x,(T . t)))
.= ((((b - a) / PI) ^2) * (((PI / (b - a)) (#) (y * T)) . t)) * (diff (((PI / (b - a)) (#) (x * T)),t)) by A32, A58, A197
.= ((((b - a) / PI) ^2) * (((PI / (b - a)) (#) (y * T)) . t)) * ((((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) . t) by A65, A197, FDIFF_1:def 7
.= (((b - a) / PI) ^2) * ((((PI / (b - a)) (#) (y * T)) . t) * ((((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) . t))
.= (((b - a) / PI) ^2) * ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) . t) by VALUED_1:5
.= (((b - a) / PI) ^2) * (((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . t) by FUNCT_1:49, A192, A194
.= ((((b - a) / PI) ^2) (#) ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) . s by VALUED_1:6 ; :: thesis:

end;

then (S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ = (((b - a) / PI) ^2) (#) ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) by A192, A193, FUNCT_1:2;
then A206: ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) | ['0,PI'] = (((b - a) / PI) ^2) (#) (((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) | ['0,PI']) by RFUNCT_1:49
.= (((b - a) / PI) ^2) (#) ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ['0,PI']) by A141, RELAT_1:74 ;
A207: ['0,PI'] c= dom ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) by A141, A191, FDIFF_1:def 7;
B207: ((PI / (b - a)) (#) (y * T)) | (dom ((PI / (b - a)) (#) (y * T))) is continuous by A80, FDIFF_1:25;
then A208: (((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ['0,PI'] is continuous by A72;
( ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) | ['0,PI'] is bounded & (S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[ is_integrable_on ['0,PI'] ) by A72, A206, A207, B207, INTEGRA5:10, INTEGRA5:11;
then A209: (S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) . PI = (integral (((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),0,PI)) + ((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) . 0) by COMPTRIG:5, A141, A191, INTEGRA7:10;
A210: ( (((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))) | ['0,PI'] is bounded & ((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))) is_integrable_on ['0,PI'] ) by A32, A33, A96, A99, A155, A208, INTEGRA5:10, INTEGRA5:11, XBOOLE_1:19;
A211: integral (((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),0,PI) = integral (((S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) `| ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[),['0,PI']) by COMPTRIG:5, INTEGRA5:def 4
.= integral (((((b - a) / PI) ^2) (#) (((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))))),['0,PI']) by A206, RFUNCT_1:49
.= integral (((((b - a) / PI) ^2) (#) (((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T)))))),0,PI) by COMPTRIG:5, INTEGRA5:def 4
.= (((b - a) / PI) ^2) * (integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI)) by A32, A33, A96, A99, A155, A210, COMPTRIG:5, INTEGRA6:10, XBOOLE_1:19 ;
A212: ( 0 in ['0,PI'] & PI in ['0,PI'] ) by A5, COMPTRIG:5;
A213: (S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) . 0 = S . ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . 0) by A141, A181, A212, FUNCT_1:13
.= S . a by A106, A141, A212, FUNCT_1:49 ;
A214: (S * (T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[)) . PI = S . ((T | ].((a1 - a) / ((b - a) / PI)),((b1 - a) / ((b - a) / PI)).[) . PI) by A141, A181, A212, FUNCT_1:13
.= S . b by A95, A141, A212, FUNCT_1:49 ;
A217: (b - a) / ((b - a) / PI) = ((b - a) / (b - a)) * PI by XCMPLX_1:82
.= 1 * PI by A3, XCMPLX_1:60
.= PI ;
A218: PI * ((b - a) / PI) = b - a by COMPTRIG:5, XCMPLX_1:87;
A219: ((b - a) / PI) * (PI / (b - a)) = 1 by A3, COMPTRIG:5, XCMPLX_1:112;
A220: for t being Real holds
( t in [.0,PI.] iff T . t in [.a,b.] )

proof

let t be Real; :: thesis:
thus ( t in [.0,PI.] implies T . t in [.a,b.] ) by A5, A88; :: thesis:
assume T . t in [.a,b.] ; :: thesis:
then (((b - a) / PI) * t) + a in [.a,b.] by A11;
then ( a <= (((b - a) / PI) * t) + a & (((b - a) / PI) * t) + a <= b ) by XXREAL_1:1;
then ( a - a <= ((((b - a) / PI) * t) + a) - a & ((((b - a) / PI) * t) + a) - a <= b - a ) by XREAL_1:9;
then ( 0 / ((b - a) / PI) <= (((b - a) / PI) * t) / ((b - a) / PI) & (((b - a) / PI) * t) / ((b - a) / PI) <= (b - a) / ((b - a) / PI) ) by COMPTRIG:5, XREAL_1:72;
then ( 0 <= t & t <= (b - a) / ((b - a) / PI) ) by A3, COMPTRIG:5, XCMPLX_1:89;
hence t in [.0,PI.] by A217; :: thesis:

end;

A221: for t being Real holds
( (t - a) / ((b - a) / PI) in [.0,PI.] iff t in [.a,b.] )

proof

let t be Real; :: thesis:

hereby :: thesis:

assume (t - a) / ((b - a) / PI) in [.0,PI.] ; :: thesis:
then ( 0 <= (t - a) / ((b - a) / PI) & (t - a) / ((b - a) / PI) <= PI ) by XXREAL_1:1;
then ( 0 * ((b - a) / PI) <= ((t - a) / ((b - a) / PI)) * ((b - a) / PI) & ((t - a) / ((b - a) / PI)) * ((b - a) / PI) <= PI * ((b - a) / PI) ) by A3, XREAL_1:64;
then ( 0 <= t - a & t - a <= PI * ((b - a) / PI) ) by A3, COMPTRIG:5, XCMPLX_1:87;
then ( 0 + a <= (t - a) + a & (t - a) + a <= (b - a) + a ) by A218, XREAL_1:7;
hence t in [.a,b.] ; :: thesis:

end;

assume t in [.a,b.] ; :: thesis:
then ( a <= t & t <= b ) by XXREAL_1:1;
then ( a - a <= t - a & t - a <= b - a ) by XREAL_1:9;
then ( 0 / ((b - a) / PI) <= (t - a) / ((b - a) / PI) & (t - a) / ((b - a) / PI) <= (b - a) / ((b - a) / PI) ) by COMPTRIG:5, XREAL_1:72;
hence (t - a) / ((b - a) / PI) in [.0,PI.] by A217; :: thesis:

end;

A222: integral ((y (#) (x `| (dom x))),a,b) <= ((1 / 2) * PI) * (((b - a) / PI) ^2) by A3, A114, A125, A131, A209, A211, A213, A214, COMPTRIG:5, XREAL_1:64;
PI * (((b - a) / PI) ^2) = (PI * ((b - a) / PI)) * ((b - a) / PI)
.= (b - a) * ((b - a) / PI) by COMPTRIG:5, XCMPLX_1:87
.= ((b - a) ^2) / PI ;
hence integral ((y (#) (x `| (dom x))),a,b) <= ((1 / 2) * ((b - a) ^2)) / PI by A222; :: thesis:

hereby :: thesis:

assume integral ((y (#) (x `| (dom x))),a,b) = ((1 / 2) * ((b - a) ^2)) / PI ; :: thesis:
then (((b - a) ^2) / (PI ^2)) * (integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI)) = ((1 / 2) * ((b - a) ^2)) / PI by A125, A131, A209, A211, A213, A214, XCMPLX_1:76;
then ((PI ^2) * (((b - a) ^2) / (PI ^2))) * (integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI)) = (PI ^2) * (((1 / 2) * ((b - a) ^2)) / PI) ;
then ((b - a) ^2) * (integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI)) = (PI * (PI * (((b - a) ^2) / PI))) * (1 / 2) by COMPTRIG:5, XCMPLX_1:87
.= (PI * ((b - a) ^2)) * (1 / 2) by LmPI, XCMPLX_1:87 ;
then integral ((((PI / (b - a)) (#) (y * T)) (#) (((PI / (b - a)) (#) (x * T)) `| (dom ((PI / (b - a)) (#) (x * T))))),0,PI) = (((1 / 2) * PI) * ((b - a) ^2)) / ((b - a) ^2) by A3, XCMPLX_1:89
.= (1 / 2) * PI by A3, XCMPLX_1:89 ;

per cases by A65, A72, A80, A87, A96, A99, A102, A110, A111, PDLAX:16;

suppose A224: for t being Real st t in [.0,PI.] holds
( ((PI / (b - a)) (#) (y * T)) . t = sin . t & ((PI / (b - a)) (#) (x * T)) . t = ((- (cos . t)) + (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) ; :: thesis:

now :: thesis:

let t be Real; :: thesis:
set s = T . t;
set u = (t - a) / ((b - a) / PI);
A225: (t - a) / ((b - a) / PI) = (PI * (t - a)) / (b - a) by XCMPLX_1:77;
A226: T . ((t - a) / ((b - a) / PI)) = (((b - a) / PI) * ((t - a) / ((b - a) / PI))) + a by A11
.= (t - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= t ;
assume t in [.a,b.] ; :: thesis:
then A227: (t - a) / ((b - a) / PI) in [.0,PI.] by A221;
then ( (x * T) . ((t - a) / ((b - a) / PI)) = x . (T . ((t - a) / ((b - a) / PI))) & (y * T) . ((t - a) / ((b - a) / PI)) = y . (T . ((t - a) / ((b - a) / PI))) ) by A5, A30, A31, A32, A33, A96, A99, FUNCT_1:12;
then ( ((PI / (b - a)) (#) (x * T)) . ((t - a) / ((b - a) / PI)) = (PI / (b - a)) * (x . t) & ((PI / (b - a)) (#) (y * T)) . ((t - a) / ((b - a) / PI)) = (PI / (b - a)) * (y . t) ) by A226, VALUED_1:6;
then ( ((b - a) / PI) * (((PI / (b - a)) (#) (x * T)) . ((t - a) / ((b - a) / PI))) = (((b - a) / PI) * (PI / (b - a))) * (x . t) & ((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . ((t - a) / ((b - a) / PI))) = (((b - a) / PI) * (PI / (b - a))) * (y . t) ) ;
hence ( y . t = ((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a))) & x . t = ((b - a) / PI) * (((- (cos . ((PI * (t - a)) / (b - a)))) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) by A113, A219, A224, A225, A227; :: thesis:

end;

hence ( for t being Real st t in [.a,b.] holds
( y . t = ((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a))) & x . t = ((b - a) / PI) * (((- (cos . ((PI * (t - a)) / (b - a)))) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) or for t being Real st t in [.a,b.] holds
( y . t = - (((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a)))) & x . t = ((b - a) / PI) * (((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ) ; :: thesis:

end;

suppose A231: for t being Real st t in [.0,PI.] holds
( ((PI / (b - a)) (#) (y * T)) . t = - (sin . t) & ((PI / (b - a)) (#) (x * T)) . t = ((cos . t) - (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) ; :: thesis:

now :: thesis:

let t be Real; :: thesis:
set s = T . t;
set u = (t - a) / ((b - a) / PI);
A232: (t - a) / ((b - a) / PI) = (PI * (t - a)) / (b - a) by XCMPLX_1:77;
A233: T . ((t - a) / ((b - a) / PI)) = (((b - a) / PI) * ((t - a) / ((b - a) / PI))) + a by A11
.= (t - a) + a by A3, COMPTRIG:5, XCMPLX_1:87
.= t ;
assume t in [.a,b.] ; :: thesis:
then A234: (t - a) / ((b - a) / PI) in [.0,PI.] by A221;
then A235: ( ((PI / (b - a)) (#) (y * T)) . ((t - a) / ((b - a) / PI)) = - (sin . ((PI * (t - a)) / (b - a))) & ((PI / (b - a)) (#) (x * T)) . ((t - a) / ((b - a) / PI)) = ((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) by A231, A232;
( (x * T) . ((t - a) / ((b - a) / PI)) = x . (T . ((t - a) / ((b - a) / PI))) & (y * T) . ((t - a) / ((b - a) / PI)) = y . (T . ((t - a) / ((b - a) / PI))) ) by A5, A30, A31, A32, A33, A96, A99, A234, FUNCT_1:12;
then ( ((PI / (b - a)) (#) (x * T)) . ((t - a) / ((b - a) / PI)) = (PI / (b - a)) * (x . t) & ((PI / (b - a)) (#) (y * T)) . ((t - a) / ((b - a) / PI)) = (PI / (b - a)) * (y . t) ) by A233, VALUED_1:6;
then ( ((b - a) / PI) * (((PI / (b - a)) (#) (x * T)) . ((t - a) / ((b - a) / PI))) = (((b - a) / PI) * (PI / (b - a))) * (x . t) & ((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . ((t - a) / ((b - a) / PI))) = (((b - a) / PI) * (PI / (b - a))) * (y . t) ) ;
hence ( y . t = - (((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a)))) & x . t = ((b - a) / PI) * (((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) by A113, A219, A235; :: thesis:

end;

assume ( for t being Real st t in [.a,b.] holds
( y . t = ((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a))) & x . t = ((b - a) / PI) * (((- (cos . ((PI * (t - a)) / (b - a)))) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) or for t being Real st t in [.a,b.] holds
( y . t = - (((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a)))) & x . t = ((b - a) / PI) * (((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ) ; :: thesis:

per cases ;

suppose A238: for t being Real st t in [.a,b.] holds
( y . t = ((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a))) & x . t = ((b - a) / PI) * (((- (cos . ((PI * (t - a)) / (b - a)))) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ; :: thesis:

now :: thesis:

let t be Real; :: thesis:
set s = T . t;
set u = (t - a) / ((b - a) / PI);
(T . t) - a = ((((b - a) / PI) * t) + a) - a by A11
.= ((b - a) / PI) * t ;
then PI * ((T . t) - a) = PI * (((b - a) / PI) * t) ;
then A239: (PI * ((T . t) - a)) / (b - a) = (((PI * (b - a)) / PI) * t) / (b - a)
.= ((b - a) * t) / (b - a) by COMPTRIG:5, XCMPLX_1:89
.= t by A3, XCMPLX_1:89 ;
assume A240: t in [.0,PI.] ; :: thesis:
then A241: T . t in [.a,b.] by A220;
( (x * T) . t = x . (T . t) & (y * T) . t = y . (T . t) ) by A5, A30, A31, A32, A33, A96, A99, A240, FUNCT_1:12;
then ( ((PI / (b - a)) (#) (x * T)) . t = (PI / (b - a)) * (x . (T . t)) & ((PI / (b - a)) (#) (y * T)) . t = (PI / (b - a)) * (y . (T . t)) ) by VALUED_1:6;
then ( ((b - a) / PI) * (((PI / (b - a)) (#) (x * T)) . t) = (((b - a) / PI) * (PI / (b - a))) * (x . (T . t)) & ((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t) = (((b - a) / PI) * (PI / (b - a))) * (y . (T . t)) ) ;
then ( (PI / (b - a)) * (((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t)) = (PI / (b - a)) * (((b - a) / PI) * (sin . t)) & (PI / (b - a)) * (((b - a) / PI) * (((PI / (b - a)) (#) (x * T)) . t)) = (PI / (b - a)) * (((b - a) / PI) * (((- (cos . t)) + (cos . 0)) + ((PI / (b - a)) * (x . a)))) ) by A219, A238, A239, A241;
then ( ((PI / (b - a)) * ((b - a) / PI)) * (((PI / (b - a)) (#) (y * T)) . t) = ((PI / (b - a)) * ((b - a) / PI)) * (sin . t) & ((PI / (b - a)) * ((b - a) / PI)) * (((PI / (b - a)) (#) (x * T)) . t) = ((PI / (b - a)) * ((b - a) / PI)) * (((- (cos . t)) + (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ;
hence ( ((PI / (b - a)) (#) (y * T)) . t = sin . t & ((PI / (b - a)) (#) (x * T)) . t = ((- (cos . t)) + (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) by A113, A219; :: thesis:

end;

hence integral ((y (#) (x `| (dom x))),a,b) = (((b - a) ^2) / (PI ^2)) * ((1 / 2) * PI) by A114, A125, A131, A209, A211, A213, A214, XCMPLX_1:76
.= ((PI * ((b - a) ^2)) / (PI ^2)) * (1 / 2)
.= ((PI / PI) * (((b - a) ^2) / PI)) * (1 / 2) by XCMPLX_1:76
.= (1 * (((b - a) ^2) / PI)) * (1 / 2) by COMPTRIG:5, XCMPLX_1:60
.= ((1 / 2) * ((b - a) ^2)) / PI ;
:: thesis:

end;

suppose A243: for t being Real st t in [.a,b.] holds
( y . t = - (((b - a) / PI) * (sin . ((PI * (t - a)) / (b - a)))) & x . t = ((b - a) / PI) * (((cos . ((PI * (t - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ; :: thesis:

now :: thesis:

let t be Real; :: thesis:
set s = T . t;
set u = (t - a) / ((b - a) / PI);
(T . t) - a = ((((b - a) / PI) * t) + a) - a by A11
.= ((b - a) / PI) * t ;
then PI * ((T . t) - a) = PI * (((b - a) / PI) * t) ;
then A244: (PI * ((T . t) - a)) / (b - a) = (((PI * (b - a)) / PI) * t) / (b - a)
.= ((b - a) * t) / (b - a) by COMPTRIG:5, XCMPLX_1:89
.= t by A3, XCMPLX_1:89 ;
assume A245: t in [.0,PI.] ; :: thesis:
then T . t in [.a,b.] by A220;
then A246: ( y . (T . t) = - (((b - a) / PI) * (sin . ((PI * ((T . t) - a)) / (b - a)))) & x . (T . t) = ((b - a) / PI) * (((cos . ((PI * ((T . t) - a)) / (b - a))) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) by A243;
( (x * T) . t = x . (T . t) & (y * T) . t = y . (T . t) ) by A5, A30, A31, A32, A33, A96, A99, A245, FUNCT_1:12;
then ( ((PI / (b - a)) (#) (x * T)) . t = (PI / (b - a)) * (x . (T . t)) & ((PI / (b - a)) (#) (y * T)) . t = (PI / (b - a)) * (y . (T . t)) ) by VALUED_1:6;
then ( ((b - a) / PI) * (((PI / (b - a)) (#) (x * T)) . t) = (((b - a) / PI) * (PI / (b - a))) * (x . (T . t)) & ((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t) = (((b - a) / PI) * (PI / (b - a))) * (y . (T . t)) ) ;
then ( (PI / (b - a)) * (((b - a) / PI) * (((PI / (b - a)) (#) (y * T)) . t)) = (PI / (b - a)) * (((b - a) / PI) * (- (sin . t))) & (PI / (b - a)) * (((b - a) / PI) * (((PI / (b - a)) (#) (x * T)) . t)) = (PI / (b - a)) * (((b - a) / PI) * (((cos . t) - (cos . 0)) + ((PI / (b - a)) * (x . a)))) ) by A219, A244, A246;
then ( (((PI / (b - a)) * (b - a)) / PI) * (((PI / (b - a)) (#) (y * T)) . t) = (((PI / (b - a)) * (b - a)) / PI) * (- (sin . t)) & (((PI / (b - a)) * (b - a)) / PI) * (((PI / (b - a)) (#) (x * T)) . t) = (((PI / (b - a)) * (b - a)) / PI) * (((cos . t) - (cos . 0)) + ((PI / (b - a)) * (x . a))) ) ;
hence ( ((PI / (b - a)) (#) (y * T)) . t = - (sin . t) & ((PI / (b - a)) (#) (x * T)) . t = ((cos . t) - (cos . 0)) + (((PI / (b - a)) (#) (x * T)) . 0) ) by A113, A219; :: thesis:

end;

hence integral ((y (#) (x `| (dom x))),a,b) = (((b - a) ^2) / (PI ^2)) * ((1 / 2) * PI) by A114, A125, A131, A209, A211, A213, A214, XCMPLX_1:76
.= ((PI * ((b - a) ^2)) / (PI ^2)) * (1 / 2)
.= ((PI / PI) * (((b - a) ^2) / PI)) * (1 / 2) by XCMPLX_1:76
.= (1 * (((b - a) ^2) / PI)) * (1 / 2) by LmPI, XCMPLX_1:60
.= ((1 / 2) * ((b - a) ^2)) / PI ;
:: thesis:

end;