let a, b, c be Real; :: thesis: ( a < b & b < c implies TriangularFS (a,b,c) is strictly-normalized )
set F = TriangularFS (a,b,c);
reconsider bb = b as Element of REAL by XREAL_0:def 1;
assume Z1: ( a < b & b < c ) ; :: thesis: TriangularFS (a,b,c) is strictly-normalized
s0: bb in [.b,c.] by Z1;
S1: TriangularFS (a,b,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.]) by Z1, TrDef;
s2: dom (AffineMap ((- (1 / (c - b))),(c / (c - b)))) = REAL by FUNCT_2:def 1;
a + 0 < b by Z1;
then T1: b - a > 0 by XREAL_1:20;
b + 0 < c by Z1;
then t1: c - b > 0 by XREAL_1:20;
bb in [.b,c.] by Z1;
then bb in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by s2, RELAT_1:57;
then A1: (TriangularFS (a,b,c)) . bb = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . bb by FUNCT_4:13, S1
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . bb by FUNCT_1:49, s0
.= 1 by Cb1, t1 ;
for y being Element of REAL st (TriangularFS (a,b,c)) . y = 1 holds
y = bb
proof
let y be Element of REAL ; :: thesis: ( (TriangularFS (a,b,c)) . y = 1 implies y = bb )
assume X0: (TriangularFS (a,b,c)) . y = 1 ; :: thesis: y = bb
per cases ( y in [.a,b.] or y in [.b,c.] or ( not y in [.a,b.] & not y in [.b,c.] ) ) ;
suppose X1: y in [.a,b.] ; :: thesis: y = bb
per cases then ( y in [.a,b.[ or y = b ) by XXREAL_1:7;
suppose x1: y in [.a,b.[ ; :: thesis: y = bb
y in REAL ;
then X3: y in dom (AffineMap ((1 / (b - a)),(- (a / (b - a))))) by FUNCT_2:def 1;
X2: y in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by X3, X1, RELAT_1:57;
not y in [.b,c.] by x1, XBOOLE_0:3, XXREAL_1:95;
then not y in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by RELAT_1:57;
then (TriangularFS (a,b,c)) . y = (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . y by FUNCT_4:11, S1
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . y by FUNCT_4:13, X2 ;
then (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . y = 1 by X1, FUNCT_1:49, X0;
hence y = bb by Hope3, T1; :: thesis: verum
end;
suppose y = b ; :: thesis: y = bb
hence y = bb ; :: thesis: verum
end;
end;
end;
suppose X1: y in [.b,c.] ; :: thesis: y = bb
y in REAL ;
then y in dom (AffineMap ((- (1 / (c - b))),(c / (c - b)))) by FUNCT_2:def 1;
then y in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by X1, RELAT_1:57;
then (TriangularFS (a,b,c)) . y = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . y by FUNCT_4:13, S1;
then (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . y = 1 by X1, FUNCT_1:49, X0;
hence y = bb by Hope4, t1; :: thesis: verum
end;
suppose so: ( not y in [.a,b.] & not y in [.b,c.] ) ; :: thesis: y = bb
then s1: ( not y in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) & not y in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) ) by RELAT_1:57;
s8: ].a,c.[ c= [.a,c.] by XXREAL_1:25;
not y in [.a,b.] \/ [.b,c.] by so, XBOOLE_0:def 3;
then not y in [.a,c.] by XXREAL_1:165, Z1;
then s7: not y in ].a,c.[ by s8;
ss: y in REAL \ ].a,c.[ by s7, XBOOLE_0:def 5;
(TriangularFS (a,b,c)) . y = (((AffineMap (0,0)) | (REAL \ ].a,c.[)) +* ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) . y by FUNCT_4:11, s1, S1
.= ((AffineMap (0,0)) | (REAL \ ].a,c.[)) . y by FUNCT_4:11, s1
.= (AffineMap (0,0)) . y by FUNCT_1:49, ss ;
hence y = bb by Hope5, X0; :: thesis: verum
end;
end;
end;
hence TriangularFS (a,b,c) is strictly-normalized by A1; :: thesis: verum