let a, b, c be Real; :: thesis: ( a < b & b < c implies integral ((TriangularFS (a,b,c)) | ['a,c']) = (c - a) / 2 )
assume A1: ( a < b & b < c ) ; :: thesis: integral ((TriangularFS (a,b,c)) | ['a,c']) = (c - a) / 2
set f = TriangularFS (a,b,c);
A2: for x being Real holds (TriangularFS (a,b,c)) . x = (1 (#) (TriangularFS (a,b,c))) . x

proof

let x be Real; :: thesis: (TriangularFS (a,b,c)) . x = (1 (#) (TriangularFS (a,b,c))) . x
thus (1 (#) (TriangularFS (a,b,c))) . x = 1 * ((TriangularFS (a,b,c)) . x) by VALUED_1:6
.= (TriangularFS (a,b,c)) . x ; :: thesis: verum

end;

integral ((TriangularFS (a,b,c)),['a,c']) = (1 * (c - a)) / 2 by A2, A1, Th6;
hence integral ((TriangularFS (a,b,c)) | ['a,c']) = (c - a) / 2 ; :: thesis: verum