let a, b, c, d be Real; :: thesis: ( c <= d implies ( integral (((id REAL) (#) (AffineMap (a,b))),['c,d']) = (d - c) * (((a * (((d * d) + (d * c)) + (c * c))) / 3) + ((b * (d + c)) / 2)) & integral ((AffineMap (a,b)),['c,d']) = (d - c) * (((a * (d + c)) / 2) + b) ) )
assume A1: c <= d ; :: thesis: ( integral (((id REAL) (#) (AffineMap (a,b))),['c,d']) = (d - c) * (((a * (((d * d) + (d * c)) + (c * c))) / 3) + ((b * (d + c)) / 2)) & integral ((AffineMap (a,b)),['c,d']) = (d - c) * (((a * (d + c)) / 2) + b) )
A2: integral (((id REAL) (#) (AffineMap (a,b))),['c,d']) = integral (((id REAL) (#) (AffineMap (a,b))),c,d) by INTEGRA5:def 4, A1
.= (((1 / 3) * a) * (((d * d) * d) - ((c * c) * c))) + (((1 / 2) * b) * ((d * d) - (c * c))) by FUZZY_6:45, A1
.= (d - c) * (((a * (((d * d) + (d * c)) + (c * c))) / 3) + ((b * (d + c)) / 2)) ;
integral ((AffineMap (a,b)),['c,d']) = integral ((AffineMap (a,b)),c,d) by INTEGRA5:def 4, A1
.= (((1 / 2) * a) * ((d ^2) - (c ^2))) + (b * (d - c)) by FUZZY_6:47, A1
.= (((1 / 2) * a) * ((d + c) * (d - c))) + (b * (d - c)) ;
hence ( integral (((id REAL) (#) (AffineMap (a,b))),['c,d']) = (d - c) * (((a * (((d * d) + (d * c)) + (c * c))) / 3) + ((b * (d + c)) / 2)) & integral ((AffineMap (a,b)),['c,d']) = (d - c) * (((a * (d + c)) / 2) + b) ) by A2; :: thesis: verum