let a, b, c be Real; :: thesis: ( a < b & b < c implies for x being Real st not x in ].a,c.[ holds
(TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x )
assume A1: ( a < b & b < c ) ; :: thesis: for x being Real st not x in ].a,c.[ holds
(TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x
set f = (AffineMap (0,0)) | (REAL \ ].a,c.[);
set fab = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set fbc = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.];
for x being Real st not x in ].a,c.[ holds
(TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x

proof

let x be Real; :: thesis: ( not x in ].a,c.[ implies (TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x )
assume B1: not x in ].a,c.[ ; :: thesis: (TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x
x in REAL by XREAL_0:def 1;
then B33: x in REAL \ ].a,c.[ by XBOOLE_0:def 5, B1;
A4: for x being object st x in (dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) /\ (dom (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) holds
((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((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.[))) /\ (dom (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) implies ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x )
assume A6: x in (dom ((AffineMap (0,0)) | (REAL \ ].a,c.[))) /\ (dom (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]))) ; :: thesis: ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x
then reconsider x = x as Real ;
( x in REAL \ ].a,c.[ & x in dom (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) ) by A6, XBOOLE_0:def 4;
then ( x in REAL \ ].a,c.[ & x in (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;
then ( x in REAL \ ].a,c.[ & x in [.a,b.] \/ (dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) ) by FUNCT_2:def 1;
then ( x in REAL \ ].a,c.[ & x in [.a,b.] \/ [.b,c.] ) by FUNCT_2:def 1;
then ( x in ].-infty,a.] \/ [.c,+infty.[ & x in [.a,c.] ) by XXREAL_1:398, XXREAL_1:165, A1;
then ( ( x in ].-infty,a.] or x in [.c,+infty.[ ) & x in [.a,c.] ) by XBOOLE_0:def 3;
then ( ( -infty < x & x <= a & a <= x & x <= c ) or ( c <= x & x < +infty & a <= x & x <= c ) ) by XXREAL_1:1, XXREAL_1:3, XXREAL_1:2;

per cases then ( x = a or x = c ) by XXREAL_0:1;

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

D1: not a in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by A1, XXREAL_1:1;
D2: a in [.a,b.] by A1;
( a in ].-infty,a.] or a in [.c,+infty.[ ) by XXREAL_1:234;
then a in ].-infty,a.] \/ [.c,+infty.[ by XBOOLE_0:def 3;
then a in REAL \ ].a,c.[ by XXREAL_1:398;
then D5: ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x = (AffineMap (0,0)) . a by FUNCT_1:49, D4
.= (0 * a) + 0 by FCONT_1:def 4
.= 0 ;
(((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . a by FUNCT_4:11, D1, D4
.= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a by FUNCT_1:49, D2
.= ((1 / (b - a)) * a) + (- (a / (b - a))) by FCONT_1:def 4
.= ((a * 1) / (b - a)) + (- (a / (b - a))) by XCMPLX_1:74
.= 0 ;
hence ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x by D5; :: thesis: verum

end;

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

E2: c in [.b,c.] by A1;
then E1: c in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by FUNCT_2:def 1;
( c in ].-infty,a.] or c in [.c,+infty.[ ) by XXREAL_1:236;
then c in ].-infty,a.] \/ [.c,+infty.[ by XBOOLE_0:def 3;
then c in REAL \ ].a,c.[ by XXREAL_1:398;
then E5: ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x = (AffineMap (0,0)) . c by FUNCT_1:49, E4
.= (0 * c) + 0 by FCONT_1:def 4
.= 0 ;
(((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . c by FUNCT_4:13, E1, E4
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c by FUNCT_1:49, E2
.= ((- (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.[)) . x = (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])) . x by E5; :: thesis: verum

end;

end;

end;

A5: x in dom ((AffineMap (0,0)) | (REAL \ ].a,c.[)) by B33, 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 (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 FUNCT_4:14
.= ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . x by A4, PARTFUN1:def 4, A5, FUNCT_4:15
.= (AffineMap (0,0)) . x by FUNCT_1:49, B33 ; :: thesis: verum

end;

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