let a, b, c be Real; :: thesis: ( a < b & b < c implies ( (TriangularFS (a,b,c)) . a = 0 & (TriangularFS (a,b,c)) . b = 1 & (TriangularFS (a,b,c)) . c = 0 ) )
assume A1: ( a < b & b < c ) ; :: thesis: ( (TriangularFS (a,b,c)) . a = 0 & (TriangularFS (a,b,c)) . b = 1 & (TriangularFS (a,b,c)) . c = 0 )
then X1a: b - b < c - b by XREAL_1:9;
set f1 = (AffineMap (0,0)) | (REAL \ ].a,c.[);
set f2 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f3 = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.];
P2: dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.a,b.] by FUNCT_2:def 1;
P3: dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.b,c.] by FUNCT_2:def 1;
then P8: not a in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by XXREAL_1:1, A1;
P9: a in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by P2, A1;
FA: (TriangularFS (a,b,c)) . a = ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . a by FUZNUM_1:def 7, A1
.= (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . a by FUNCT_4:11, P8
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . a by FUNCT_4:13, P9
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a by FUNCT_1:47, P9
.= ((1 / (b - a)) * a) + (- (a / (b - a))) by FCONT_1:def 4
.= ((a * 1) / (b - a)) + (- (a / (b - a))) by XCMPLX_1:74
.= 0 ;
B0: b in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by P3, A1;
FB: (TriangularFS (a,b,c)) . b = ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . b by FUZNUM_1:def 7, A1
.= ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . b by FUNCT_4:13, B0
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b by FUNCT_1:47, B0
.= ((- (1 / (c - b))) * b) + (c / (c - b)) by FCONT_1:def 4
.= (- (b * (1 / (c - b)))) + (c / (c - b))
.= (- ((b * 1) / (c - b))) + (c / (c - b)) by XCMPLX_1:74
.= ((- b) / (c - b)) + (c / (c - b)) by XCMPLX_1:187
.= ((- b) + c) / (c - b) by XCMPLX_1:62
.= 1 by XCMPLX_1:60, X1a ;
C0: c in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by P3, A1;
(TriangularFS (a,b,c)) . c = ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . c by FUZNUM_1:def 7, A1
.= ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . c by FUNCT_4:13, C0
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c by FUNCT_1:47, C0
.= ((- (1 / (c - b))) * c) + (c / (c - b)) by FCONT_1:def 4
.= (- (c * (1 / (c - b)))) + (c / (c - b))
.= (- ((c * 1) / (c - b))) + (c / (c - b)) by XCMPLX_1:74
.= 0 ;
hence ( (TriangularFS (a,b,c)) . a = 0 & (TriangularFS (a,b,c)) . b = 1 & (TriangularFS (a,b,c)) . c = 0 ) by FA, FB; :: thesis: verum