let a, b, c be Real; :: thesis: ( a < b & b < c implies for x being Real st x in [.b,c.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x )
assume A1: ( a < b & b < c ) ; :: thesis: for x being Real st x in [.b,c.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x
let x be Real; :: thesis: ( x in [.b,c.] implies (TriangularFS (a,b,c)) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x )
assume B1: x in [.b,c.] ; :: thesis: (TriangularFS (a,b,c)) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x
then B21: x in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by FUNCT_2:def 1;
thus (TriangularFS (a,b,c)) . x = ((((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x by A1, FUZNUM_1:def 7
.= ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x by B21, FUNCT_4:13
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x by B1, FUNCT_1:49 ; :: thesis: verum