let a, b, c be Real; :: thesis: ( a < b & b < c implies for x being Real st x in [.a,b.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x )
assume A1: ( a < b & b < c ) ; :: thesis: for x being Real st x in [.a,b.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x
then A2: b - a <> 0 ;
A3: c - b <> 0 by A1;
C3: c in [.b,c.] by A1;
for x being Real st x in [.a,b.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x

proof

let x be Real; :: thesis: ( x in [.a,b.] implies (TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x )
assume A4: x in [.a,b.] ; :: thesis: (TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x
B10: dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) = (dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_4:def 1
.= (REAL \ ].a,c.[) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by FUNCT_2:def 1
.= (REAL \ ].a,c.[) \/ [.a,b.] by FUNCT_2:def 1 ;
B12: x in dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) by B10, A4, XBOOLE_0:def 3;
B13: x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by FUNCT_2:def 1, A4;
B11: ((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) tolerates (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]

proof

for x being object st x in (dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) holds
(((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x

proof

let x be object ; :: thesis: ( x in (dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) implies (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x )
assume B111: x in (dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) ; :: thesis: (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x
then reconsider x = x as Real ;
(dom (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) = ((dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_4:def 1
.= ((REAL \ ].a,c.[) \/ (dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]))) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_2:def 1
.= ((REAL \ ].a,c.[) \/ [.a,b.]) /\ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) by FUNCT_2:def 1
.= ((REAL \ ].a,c.[) \/ [.a,b.]) /\ [.b,c.] by FUNCT_2:def 1 ;
then X1: ( x in (REAL \ ].a,c.[) \/ [.a,b.] & x in [.b,c.] ) by XBOOLE_0:def 4, B111;

per cases ( ( x in REAL \ ].a,c.[ & x in [.b,c.] ) or ( x in [.a,b.] & x in [.b,c.] ) ) by X1, XBOOLE_0:def 3;

suppose ( x in REAL \ ].a,c.[ & x in [.b,c.] ) ; :: thesis: (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x

then ( x in ].-infty,a.] \/ [.c,+infty.[ & x in [.b,c.] ) by XXREAL_1:398;
then ( ( x in ].-infty,a.] & x in [.b,c.] ) or ( x in [.c,+infty.[ & x in [.b,c.] ) ) by XBOOLE_0:def 3;
then ( ( -infty < x & x <= a & b <= x & x <= c ) or ( c <= x & x < +infty & b <= x & x <= c ) ) by XXREAL_1:1, XXREAL_1:3, XXREAL_1:2;
then ( x in [.b,a.] or x in [.c,c.] ) ;
then C1: x in {c} by XXREAL_1:17, XXREAL_1:29, A1;
C2: not c in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by A1, XXREAL_1:1;
( c <= c & c < +infty ) by XXREAL_0:9, XREAL_0:def 1;
then ( c in ].-infty,a.] or c in [.c,+infty.[ ) ;
then c in ].-infty,a.] \/ [.c,+infty.[ by XBOOLE_0:def 3;
then C4: c in REAL \ ].a,c.[ by XXREAL_1:398;
C5: (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . c by C1, TARSKI:def 1
.= ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . c by C2, FUNCT_4:11
.= (AffineMap (0,0)) . c by C4, FUNCT_1:49
.= (0 * c) + 0 by FCONT_1:def 4 ;
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . c by C1, TARSKI:def 1
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c by C3, FUNCT_1:49
.= ((- (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 (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x by C5; :: thesis: verum

end;

suppose Z1: ( x in [.a,b.] & x in [.b,c.] ) ; :: thesis: (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x

then B113: ( a <= x & x <= b & b <= x & x <= c ) by XXREAL_1:1;
B114: x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by FUNCT_2:def 1, Z1;
B112: (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . x by FUNCT_4:13, B114
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x by Z1, FUNCT_1:49
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b by B113, XXREAL_0:1
.= ((1 / (b - a)) * b) + (- (a / (b - a))) by FCONT_1:def 4
.= (b * (1 / (b - a))) - ((a * 1) / (b - a))
.= (b * (1 / (b - a))) - (a * (1 / (b - a))) by XCMPLX_1:74
.= (b - a) * (1 / (b - a))
.= ((b - a) * 1) / (b - a) by XCMPLX_1:74
.= 1 by A2, XCMPLX_1:60 ;
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x by Z1, FUNCT_1:49
.= ((- (1 / (c - b))) * x) + (c / (c - b)) by FCONT_1:def 4
.= ((- (1 / (c - b))) * b) + (c / (c - b)) by B113, XXREAL_0:1
.= ((c * 1) / (c - b)) - (b * (1 / (c - b)))
.= (c * (1 / (c - b))) - (b * (1 / (c - b))) by XCMPLX_1:74
.= (c - b) * (1 / (c - b))
.= ((c - b) * 1) / (c - b) by XCMPLX_1:74
.= 1 by A3, XCMPLX_1:60 ;
hence (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x by B112; :: thesis: verum

end;

end;

end;

hence ((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) tolerates (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.] by PARTFUN1:def 4; :: thesis: verum

end;

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 (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . x by FUNCT_4:15, B12, B11
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . x by FUNCT_4:13, B13
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x by A4, FUNCT_1:49 ; :: thesis: verum

end;

hence for x being Real st x in [.a,b.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x ; :: thesis: verum