let a, b, c be Real; :: thesis: ( a < b & c > 0 implies centroid ((AffineMap (0,c)),['a,b']) = (a + b) / 2 )
assume A1: a < b ; :: thesis: ( not c > 0 or centroid ((AffineMap (0,c)),['a,b']) = (a + b) / 2 )
assume A2: c > 0 ; :: thesis: centroid ((AffineMap (0,c)),['a,b']) = (a + b) / 2
R1: [#] REAL = REAL by SUBSET_1:def 3;
R2: ['a,b'] c= REAL ;
then B1: ['a,b'] c= [#] REAL by SUBSET_1:def 3;
set f = AffineMap (c,0);
LU1: ( ['a,b'] = [.(lower_bound ['a,b']),(upper_bound ['a,b']).] & ['a,b'] = [.a,b.] ) by A1, INTEGRA5:def 3, INTEGRA1:4;
set F = (c / 2) (#) (#Z 2);
D3: dom ((id REAL) (#) (AffineMap (0,c))) = REAL by FUNCT_2:def 1;
D5A: dom ((c / 2) (#) (#Z 2)) = REAL by FUNCT_2:def 1;
D6A: dom (#Z 2) = REAL by FUNCT_2:def 1;
for x being Real st x in [#] REAL holds
#Z 2 is_differentiable_in x by TAYLOR_1:2;
then C4A: #Z 2 is_differentiable_on [#] REAL by FDIFF_1:9, D6A;
then C4: (c / 2) (#) (#Z 2) is_differentiable_on [#] REAL by FDIFF_1:20, D5A;
then E7: dom (((c / 2) (#) (#Z 2)) `| ([#] REAL)) = [#] REAL by FDIFF_1:def 7;
C1A: for x being Element of REAL st x in dom (((c / 2) (#) (#Z 2)) `| ([#] REAL)) holds
(((c / 2) (#) (#Z 2)) `| ([#] REAL)) . x = ((id REAL) (#) (AffineMap (0,c))) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (((c / 2) (#) (#Z 2)) `| ([#] REAL)) implies (((c / 2) (#) (#Z 2)) `| ([#] REAL)) . x = ((id REAL) (#) (AffineMap (0,c))) . x )
assume E4: x in dom (((c / 2) (#) (#Z 2)) `| ([#] REAL)) ; :: thesis: (((c / 2) (#) (#Z 2)) `| ([#] REAL)) . x = ((id REAL) (#) (AffineMap (0,c))) . x
E3: x in [#] REAL by E4, C4, FDIFF_1:def 7;
E2: #Z 2 is_differentiable_in x by TAYLOR_1:2;
E5: (((c / 2) (#) (#Z 2)) `| ([#] REAL)) . x = diff (((c / 2) (#) (#Z 2)),x) by FDIFF_1:def 7, C4, E3
.= (c / 2) * (diff ((#Z 2),x)) by FDIFF_1:15, E2
.= (c / 2) * (2 * (x #Z (2 - 1))) by TAYLOR_1:2
.= (c / 2) * (2 * x) by PREPOWER:35
.= c * x ;
((id REAL) (#) (AffineMap (0,c))) . x = ((id REAL) . x) * ((AffineMap (0,c)) . x) by VALUED_1:5
.= x * ((0 * x) + c) by FCONT_1:def 4
.= c * x ;
hence (((c / 2) (#) (#Z 2)) `| ([#] REAL)) . x = ((id REAL) (#) (AffineMap (0,c))) . x by E5; :: thesis: verum

end;

set F2 = (id REAL) (#) (AffineMap (0,c));
reconsider F2 = (id REAL) (#) (AffineMap (0,c)) as PartFunc of REAL,REAL ;
F2 | ['a,b'] is continuous ;
then ( (id REAL) (#) (AffineMap (0,c)) is_integrable_on ['a,b'] & F2 | ['a,b'] is bounded ) by INTEGRA5:10, INTEGRA5:11, D3;
then C2: ( ((c / 2) (#) (#Z 2)) `| ([#] REAL) is_integrable_on ['a,b'] & (((c / 2) (#) (#Z 2)) `| ([#] REAL)) | ['a,b'] is bounded ) by PARTFUN1:5, SUBSET_1:def 3, D3, E7, C1A;
C3: integral (((id REAL) (#) (AffineMap (0,c))),['a,b']) = integral ((((c / 2) (#) (#Z 2)) `| ([#] REAL)),['a,b']) by PARTFUN1:5, SUBSET_1:def 3, D3, E7, C1A
.= (((c / 2) (#) (#Z 2)) . (upper_bound ['a,b'])) - (((c / 2) (#) (#Z 2)) . (lower_bound ['a,b'])) by INTEGRA5:13, B1, C2, C4A, FDIFF_1:20, D5A
.= (((c / 2) (#) (#Z 2)) . b) - (((c / 2) (#) (#Z 2)) . (lower_bound ['a,b'])) by LU1, INTEGRA1:5
.= (((c / 2) (#) (#Z 2)) . b) - (((c / 2) (#) (#Z 2)) . a) by LU1, INTEGRA1:5
.= ((c / 2) * ((#Z 2) . b)) - (((c / 2) (#) (#Z 2)) . a) by VALUED_1:6
.= ((c / 2) * ((#Z 2) . b)) - ((c / 2) * ((#Z 2) . a)) by VALUED_1:6
.= ((c / 2) * (b #Z 2)) - ((c / 2) * ((#Z 2) . a)) by TAYLOR_1:def 1
.= ((c / 2) * (b #Z 2)) - ((c / 2) * (a #Z 2)) by TAYLOR_1:def 1
.= ((c / 2) * (b |^ 2)) - ((c / 2) * (a #Z 2)) by PREPOWER:36
.= ((c / 2) * (b |^ 2)) - ((c / 2) * (a |^ 2)) by PREPOWER:36
.= ((c / 2) * (b ^2)) - ((c / 2) * (a |^ 2)) by NEWTON:81
.= ((c / 2) * (b ^2)) - ((c / 2) * (a ^2)) by NEWTON:81
.= ((b + a) / 2) * (c * (b - a)) ;
A4: [#] REAL c= dom (AffineMap (c,0)) by R1, FUNCT_2:def 1;
A5: for x being Real st x in [#] REAL holds
(AffineMap (c,0)) . x = (c * x) + 0 by FCONT_1:def 4;
then B6: AffineMap (c,0) is_differentiable_on [#] REAL by A4, FDIFF_1:23;
D4: dom ((AffineMap (c,0)) `| ([#] REAL)) = [#] REAL by B6, FDIFF_1:def 7;
then dom ((AffineMap (c,0)) `| ([#] REAL)) = REAL by SUBSET_1:def 3;
then B5: dom ((AffineMap (c,0)) `| ([#] REAL)) = dom (AffineMap (0,c)) by FUNCT_2:def 1;
B3A: for x being Element of REAL st x in dom ((AffineMap (c,0)) `| ([#] REAL)) holds
((AffineMap (c,0)) `| ([#] REAL)) . x = (AffineMap (0,c)) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((AffineMap (c,0)) `| ([#] REAL)) implies ((AffineMap (c,0)) `| ([#] REAL)) . x = (AffineMap (0,c)) . x )
assume x in dom ((AffineMap (c,0)) `| ([#] REAL)) ; :: thesis: ((AffineMap (c,0)) `| ([#] REAL)) . x = (AffineMap (0,c)) . x
then ((AffineMap (c,0)) `| ([#] REAL)) . x = (0 * x) + c by D4, A5, A4, FDIFF_1:23
.= (AffineMap (0,c)) . x by FCONT_1:def 4 ;
hence ((AffineMap (c,0)) `| ([#] REAL)) . x = (AffineMap (0,c)) . x ; :: thesis: verum

end;

B21: ['a,b'] c= dom (AffineMap (0,c)) by FUNCT_2:def 1, R2;
set F3 = AffineMap (0,c);
reconsider F3 = AffineMap (0,c) as PartFunc of REAL,REAL ;
F3 | ['a,b'] is continuous ;
then ( AffineMap (0,c) is_integrable_on ['a,b'] & (AffineMap (0,c)) | ['a,b'] is bounded ) by INTEGRA5:10, INTEGRA5:11, B21;
then B2: ( (AffineMap (c,0)) `| ([#] REAL) is_integrable_on ['a,b'] & ((AffineMap (c,0)) `| ([#] REAL)) | ['a,b'] is bounded ) by B5, PARTFUN1:5, B3A;
B4: integral ((AffineMap (0,c)),['a,b']) = integral (((AffineMap (c,0)) `| ([#] REAL)),['a,b']) by B5, PARTFUN1:5, B3A
.= ((AffineMap (c,0)) . (upper_bound ['a,b'])) - ((AffineMap (c,0)) . (lower_bound ['a,b'])) by INTEGRA5:13, B1, B2, A5, A4, FDIFF_1:23
.= ((AffineMap (c,0)) . b) - ((AffineMap (c,0)) . (lower_bound ['a,b'])) by LU1, INTEGRA1:5
.= ((AffineMap (c,0)) . b) - ((AffineMap (c,0)) . a) by LU1, INTEGRA1:5
.= ((c * b) + 0) - ((AffineMap (c,0)) . a) by FCONT_1:def 4
.= (c * b) - ((c * a) + 0) by FCONT_1:def 4
.= c * (b - a) ;
a - a < b - a by A1, XREAL_1:9;
hence centroid ((AffineMap (0,c)),['a,b']) = (a + b) / 2 by XCMPLX_1:89, A2, B4, C3; :: thesis: verum