let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies ( (TrapezoidalFS (a,b,c,d)) . a = 0 & (TrapezoidalFS (a,b,c,d)) . b = 1 & (TrapezoidalFS (a,b,c,d)) . c = 1 & (TrapezoidalFS (a,b,c,d)) . d = 0 ) )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: ( (TrapezoidalFS (a,b,c,d)) . a = 0 & (TrapezoidalFS (a,b,c,d)) . b = 1 & (TrapezoidalFS (a,b,c,d)) . c = 1 & (TrapezoidalFS (a,b,c,d)) . d = 0 )
then AA1: a in [.a,b.] ;
set f1 = (AffineMap (0,0)) | (REAL \ ].a,d.[);
set f2 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f3 = (AffineMap (0,1)) | [.b,c.];
set f4 = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
D2: dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.a,b.] by FUNCT_2:def 1;
D3: dom ((AffineMap (0,1)) | [.b,c.]) = [.b,c.] by FUNCT_2:def 1;
D4: dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = [.c,d.] by FUNCT_2:def 1;
AA2: a in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by D2, A1;
AA4: dom (((AffineMap (0,1)) | [.b,c.]) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = (dom ((AffineMap (0,1)) | [.b,c.])) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by FUNCT_4:def 1
.= [.b,c.] \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by FUNCT_2:def 1
.= [.b,c.] \/ [.c,d.] by FUNCT_2:def 1
.= [.b,d.] by XXREAL_1:165, A1 ;
AA3: not a in dom (((AffineMap (0,1)) | [.b,c.]) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) by AA4, XXREAL_1:1, A1;
AA: (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . a = ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* (((AffineMap (0,1)) | [.b,c.]) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))) . a by FUNCT_4:14
.= (((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . a by FUNCT_4:11, AA3
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . a by FUNCT_4:13, AA2
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a by FUNCT_1:49, AA1
.= 0 by FUZNUM_1:2 ;
B1: b in [.b,c.] by A1;
B0: b in dom ((AffineMap (0,1)) | [.b,c.]) by D3, A1;
B2: not b in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by D4, XXREAL_1:1, A1;
BB: (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . b = ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) . b by FUNCT_4:11, B2
.= ((AffineMap (0,1)) | [.b,c.]) . b by FUNCT_4:13, B0
.= (AffineMap (0,1)) . b by FUNCT_1:49, B1
.= (0 * b) + 1 by FCONT_1:def 4
.= 1 ;
A4: d - c <> 0 by A1;
C2: c in [.c,d.] by A1;
C1: c in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by D4, A1;
CC: (((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . c = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . c by FUNCT_4:13, C1
.= (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . c by FUNCT_1:49, C2
.= 1 by FUZNUM_1:4, A4 ;
AD1: d in [.c,d.] by A1;
AD2: d in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) by D4, A1;
(((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . d = ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . d by FUNCT_4:13, AD2
.= (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . d by FUNCT_1:49, AD1
.= 0 by FUZNUM_1:5 ;
hence ( (TrapezoidalFS (a,b,c,d)) . a = 0 & (TrapezoidalFS (a,b,c,d)) . b = 1 & (TrapezoidalFS (a,b,c,d)) . c = 1 & (TrapezoidalFS (a,b,c,d)) . d = 0 ) by AA, BB, CC, FUZNUM_1:def 8, A1; :: thesis: verum