let a, b, c be Real; ( 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 )
; 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 ;
( (TriangularFS (a,b,c)) . y = 1 implies y = bb )
assume X0:
(TriangularFS (a,b,c)) . y = 1
;
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.]
;
y = bbper cases then
( y in [.a,b.[ or y = b )
by XXREAL_1:7;
suppose x1:
y in [.a,b.[
;
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;
verum end; end; end; suppose X1:
y in [.b,c.]
;
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;
verum end; suppose so:
( not
y in [.a,b.] & not
y in [.b,c.] )
;
y = bbthen 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;
verum end; end;
end;
hence
TriangularFS (a,b,c) is strictly-normalized
by A1; verum