let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies (TriangularFS (a,b,c)) + (TriangularFS (b,c,d)) = TrapezoidalFS (a,b,c,d) )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: (TriangularFS (a,b,c)) + (TriangularFS (b,c,d)) = TrapezoidalFS (a,b,c,d)
then CB: b - b < c - b by XREAL_1:9;
A2: dom ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) = (dom (TriangularFS (a,b,c))) /\ (dom (TriangularFS (b,c,d))) by VALUED_1:def 1
.= REAL /\ (dom (TriangularFS (b,c,d))) by FUNCT_2:def 1
.= REAL /\ REAL by FUNCT_2:def 1
.= dom (TrapezoidalFS (a,b,c,d)) by FUNCT_2:def 1 ;
for x being object st x in dom (TrapezoidalFS (a,b,c,d)) holds
((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

proof

let x be object ; :: thesis: ( x in dom (TrapezoidalFS (a,b,c,d)) implies ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x )
assume A3: x in dom (TrapezoidalFS (a,b,c,d)) ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x
then reconsider x = x as Real ;
A4: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = ((TriangularFS (a,b,c)) . x) + ((TriangularFS (b,c,d)) . x) by VALUED_1:def 1, A2, A3;

per cases ( x in [.a,d.] or not x in [.a,d.] ) ;

suppose x in [.a,d.] ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

then B01: ( a <= x & x <= d ) by XXREAL_1:1;

per cases ( c <= x or x < c ) ;

suppose B1: c <= x ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

then B11: x in [.c,d.] by B01;
not x in ].a,c.[ by B1, XXREAL_1:4;
then (TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x by FUZZY_8:48, A1
.= (0 * x) + 0 by FCONT_1:def 4 ;
then ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) . x by B11, A1, FUZZY_8:47, A4;
hence ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x by Th22, B11, A1; :: thesis: verum

end;

suppose B2: x < c ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

per cases ( b <= x or x < b ) ;

suppose b <= x ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

then B211: x in [.b,c.] by B2;
((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = ((TriangularFS (a,b,c)) . x) + ((TriangularFS (b,c,d)) . x) by VALUED_1:def 1, A2, A3
.= ((TriangularFS (a,b,c)) . x) + ((AffineMap ((1 / (c - b)),(- (b / (c - b))))) . x) by B211, A1, FUZZY_8:46
.= ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x) + ((AffineMap ((1 / (c - b)),(- (b / (c - b))))) . x) by B211, A1, FUZZY_8:47
.= ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x) + (((1 / (c - b)) * x) + (- (b / (c - b)))) by FCONT_1:def 4
.= (((- (1 / (c - b))) * x) + (c / (c - b))) + (((1 / (c - b)) * x) + (- (b / (c - b)))) by FCONT_1:def 4
.= (c / (c - b)) - (b / (c - b))
.= (c - b) / (c - b) by XCMPLX_1:120
.= (0 * x) + 1 by XCMPLX_1:60, CB
.= (AffineMap (0,1)) . x by FCONT_1:def 4
.= (TrapezoidalFS (a,b,c,d)) . x by B211, A1, Th21 ;
hence ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x ; :: thesis: verum

end;

suppose B22: x < b ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

then B221: x in [.a,b.] by B01;
not x in ].b,d.[ by XXREAL_1:4, B22;
then ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = ((TriangularFS (a,b,c)) . x) + ((AffineMap (0,0)) . x) by A4, A1, FUZZY_8:48
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x) + ((AffineMap (0,0)) . x) by A1, B221, FUZZY_8:46
.= ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x) + ((0 * x) + 0) by FCONT_1:def 4
.= (TrapezoidalFS (a,b,c,d)) . x by A1, Th20, B221 ;
hence ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x ; :: thesis: verum

end;

end;

end;

end;

end;

suppose not x in [.a,d.] ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

per cases then ( x < a or d < x ) ;

suppose C11: x < a ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

then C12: not x in ].a,c.[ by XXREAL_1:4;
C14: not x in [.a,d.] by XXREAL_1:1, C11;
x < b by A1, C11, XXREAL_0:2;
then C13: not x in ].b,d.[ by XXREAL_1:4;
((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = ((TriangularFS (a,b,c)) . x) + ((TriangularFS (b,c,d)) . x) by VALUED_1:def 1, A2, A3
.= ((TriangularFS (a,b,c)) . x) + ((AffineMap (0,0)) . x) by A1, C13, FUZZY_8:48
.= ((AffineMap (0,0)) . x) + ((AffineMap (0,0)) . x) by A1, C12, FUZZY_8:48
.= ((AffineMap (0,0)) . x) + ((0 * x) + 0) by FCONT_1:def 4
.= ((0 * x) + 0) + 0 by FCONT_1:def 4
.= (TrapezoidalFS (a,b,c,d)) . x by C14, A1, Th23 ;
hence ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x ; :: thesis: verum

end;

suppose C2: d < x ; :: thesis: ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x

then C21: not x in ].b,d.[ by XXREAL_1:4;
C22: not x in [.a,d.] by XXREAL_1:1, C2;
c < x by A1, C2, XXREAL_0:2;
then C23: not x in ].a,c.[ by XXREAL_1:4;
((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = ((TriangularFS (a,b,c)) . x) + ((TriangularFS (b,c,d)) . x) by VALUED_1:def 1, A2, A3
.= ((TriangularFS (a,b,c)) . x) + ((AffineMap (0,0)) . x) by A1, C21, FUZZY_8:48
.= ((AffineMap (0,0)) . x) + ((AffineMap (0,0)) . x) by A1, C23, FUZZY_8:48
.= ((AffineMap (0,0)) . x) + ((0 * x) + 0) by FCONT_1:def 4
.= ((0 * x) + 0) + 0 by FCONT_1:def 4
.= (TrapezoidalFS (a,b,c,d)) . x by C22, A1, Th23 ;
hence ((TriangularFS (a,b,c)) + (TriangularFS (b,c,d))) . x = (TrapezoidalFS (a,b,c,d)) . x ; :: thesis: verum

end;

end;

end;

end;

end;

hence (TriangularFS (a,b,c)) + (TriangularFS (b,c,d)) = TrapezoidalFS (a,b,c,d) by A2, FUNCT_1:2; :: thesis: verum