let a, b, c, d, r be Real; :: thesis: ( a < b & b < c & c < d implies (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) = (r (#) (TrapezoidalFS (a,b,c,d))) | [.a,d.] )
assume that
Z1: a < b and
Z2: b < c and
Z3: c < d ; :: thesis: (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) = (r (#) (TrapezoidalFS (a,b,c,d))) | [.a,d.]
Z4: a < c by XXREAL_0:2, Z1, Z2;
set f1 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f2 = (AffineMap (0,1)) | [.b,c.];
set f3 = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
A1: (r (#) (TrapezoidalFS (a,b,c,d))) | [.a,d.] = (r (#) (TrapezoidalFS (a,b,c,d))) | ['a,d'] by INTEGRA5:def 3, XXREAL_0:2, Z3, Z4
.= r (#) ((TrapezoidalFS (a,b,c,d)) | ['a,d']) by Th27
.= r (#) ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) by INTEGRA5:def 3, XXREAL_0:2, Z3, Z4
.= r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by LmSymTrape2, Z1, Z2, Z3 ;
set F1 = AffineMap ((1 / (b - a)),(- (a / (b - a))));
set F2 = AffineMap (0,1);
set F3 = AffineMap ((- (1 / (d - c))),(d / (d - c)));
D2: [.a,d.] = dom (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by A1, FUNCT_2:def 1;
D1: dom ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) = dom ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | ['a,b']) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) by INTEGRA5:def 3, Z1
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) by Th27
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* ((r (#) (AffineMap (0,1))) | ['b,c'])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) by INTEGRA5:def 3, Z2
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* (r (#) ((AffineMap (0,1)) | ['b,c']))) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) by Th27
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* (r (#) ((AffineMap (0,1)) | ['b,c']))) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | ['c,d'])) by INTEGRA5:def 3, Z3
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) +* (r (#) ((AffineMap (0,1)) | ['b,c']))) +* (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | ['c,d']))) by Th27
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (r (#) ((AffineMap (0,1)) | ['b,c']))) +* (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | ['c,d']))) by INTEGRA5:def 3, Z1
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (r (#) ((AffineMap (0,1)) | [.b,c.]))) +* (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | ['c,d']))) by INTEGRA5:def 3, Z2
.= dom (((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (r (#) ((AffineMap (0,1)) | [.b,c.]))) +* (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by INTEGRA5:def 3, Z3
.= (dom ((r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (r (#) ((AffineMap (0,1)) | [.b,c.])))) \/ (dom (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by FUNCT_4:def 1
.= ((dom (r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) \/ (dom (r (#) ((AffineMap (0,1)) | [.b,c.])))) \/ (dom (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by FUNCT_4:def 1
.= ([.a,b.] \/ (dom (r (#) ((AffineMap (0,1)) | [.b,c.])))) \/ (dom (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by FUNCT_2:def 1
.= ([.a,b.] \/ [.b,c.]) \/ (dom (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) by FUNCT_2:def 1
.= ([.a,b.] \/ [.b,c.]) \/ [.c,d.] by FUNCT_2:def 1
.= [.a,c.] \/ [.c,d.] by XXREAL_1:165, Z1, Z2
.= [.a,d.] by XXREAL_1:165, Z4, Z3 ;
for x being object st x in dom (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) holds
((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x

proof

let x be object ; :: thesis: ( x in dom (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) implies ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x )
assume P0: x in dom (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) ; :: thesis: ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x
then reconsider x = x as Real by D2;
P1: ( a <= x & x <= d ) by XXREAL_1:1, P0, D2;

per cases ( c <= x or x < c ) ;

suppose c <= x ; :: thesis: ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x

then P21: x in [.c,d.] by P1;
then P22: x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by FUNCT_2:def 1;
P23: x in dom ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) by FUNCT_2:def 1, P21;
((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) . x by FUNCT_4:13, P23
.= ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | ['c,d']) . x by INTEGRA5:def 3, Z3
.= (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | ['c,d'])) . x by Th27
.= (r (#) ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x by INTEGRA5:def 3, Z3
.= r * (((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x) by VALUED_1:6
.= r * (((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x) by FUNCT_4:13, P22 ;
hence ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x by VALUED_1:6; :: thesis: verum

end;

suppose P3: x < c ; :: thesis: ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x

then P32: not x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by XXREAL_1:1;
P33: not x in dom ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) by XXREAL_1:1, P3;
Q1: (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x = r * (((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x) by VALUED_1:6
.= r * ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) . x) by FUNCT_4:11, P32 ;

per cases ( b <= x or x < b ) ;

suppose b <= x ; :: thesis: ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x

then R11: x in [.b,c.] by P3;
then R12: x in dom ((AffineMap (0,1)) | [.b,c.]) by FUNCT_2:def 1;
R13: x in dom ((r (#) (AffineMap (0,1))) | [.b,c.]) by FUNCT_2:def 1, R11;
(r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x = r * (((AffineMap (0,1)) | [.b,c.]) . x) by FUNCT_4:13, R12, Q1
.= (r (#) ((AffineMap (0,1)) | [.b,c.])) . x by VALUED_1:6
.= (r (#) ((AffineMap (0,1)) | ['b,c'])) . x by INTEGRA5:def 3, Z2
.= ((r (#) (AffineMap (0,1))) | ['b,c']) . x by Th27
.= ((r (#) (AffineMap (0,1))) | [.b,c.]) . x by INTEGRA5:def 3, Z2
.= (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) . x by FUNCT_4:13, R13 ;
hence ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x by FUNCT_4:11, P33; :: thesis: verum

end;

suppose R2: x < b ; :: thesis: ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x

then R22: not x in dom ((AffineMap (0,1)) | [.b,c.]) by XXREAL_1:1;
R23: not x in dom ((r (#) (AffineMap (0,1))) | [.b,c.]) by XXREAL_1:1, R2;
((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) . x by FUNCT_4:11, P33
.= ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) . x by FUNCT_4:11, R23
.= ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | ['a,b']) . x by INTEGRA5:def 3, Z1
.= (r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ['a,b'])) . x by Th27
.= (r (#) ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x by INTEGRA5:def 3, Z1
.= r * (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . x) by VALUED_1:6
.= (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x by Q1, FUNCT_4:11, R22 ;
hence ((((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.])) . x = (r (#) ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . x ; :: thesis: verum

end;

end;

end;

end;

end;

hence (((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap (0,1))) | [.b,c.])) +* ((r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))) | [.c,d.]) = (r (#) (TrapezoidalFS (a,b,c,d))) | [.a,d.] by FUNCT_1:2, D1, D2, A1; :: thesis: verum