let f, g, h be Function of REAL,REAL; :: thesis: for a, b, c being Real st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & integral (f,['a,b']) <> 0 & integral (g,['b,c']) <> 0 & f . b = g . b holds
centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c']))))
let a, b, c be Real; :: thesis: ( a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & integral (f,['a,b']) <> 0 & integral (g,['b,c']) <> 0 & f . b = g . b implies centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c'])))) )
assume that
A1: ( a <= b & b <= c ) and
A2: ( f is continuous & g is continuous ) and
A3: h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) ; :: thesis: ( not integral (f,['a,b']) <> 0 or not integral (g,['b,c']) <> 0 or not f . b = g . b or centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c'])))) )
assume A4: ( integral (f,['a,b']) <> 0 & integral (g,['b,c']) <> 0 ) ; :: thesis: ( not f . b = g . b or centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c'])))) )
assume A6: f . b = g . b ; :: thesis: centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c']))))
A5: ((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c']))) = (((integral (((id REAL) (#) f),['a,b'])) / (integral (f,['a,b']))) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c']))) by FUZZY_6:def 1
.= (((integral (((id REAL) (#) f),['a,b'])) / (integral (f,['a,b']))) * (integral (f,['a,b']))) + (((integral (((id REAL) (#) g),['b,c'])) / (integral (g,['b,c']))) * (integral (g,['b,c']))) by FUZZY_6:def 1
.= ((integral (((id REAL) (#) f),['a,b'])) / ((integral (f,['a,b'])) / (integral (f,['a,b'])))) + (((integral (((id REAL) (#) g),['b,c'])) / (integral (g,['b,c']))) * (integral (g,['b,c']))) by XCMPLX_1:82
.= ((integral (((id REAL) (#) f),['a,b'])) / 1) + (((integral (((id REAL) (#) g),['b,c'])) / (integral (g,['b,c']))) * (integral (g,['b,c']))) by XCMPLX_1:60, A4
.= ((integral (((id REAL) (#) f),['a,b'])) / 1) + ((integral (((id REAL) (#) g),['b,c'])) / ((integral (g,['b,c'])) / (integral (g,['b,c'])))) by XCMPLX_1:82
.= (integral (((id REAL) (#) f),['a,b'])) + ((integral (((id REAL) (#) g),['b,c'])) / 1) by XCMPLX_1:60, A4
.= integral (((id REAL) (#) h),['a,c']) by FUZZY_7:43, A1, A2, A3, A6 ;
centroid (h,['a,c']) = (integral (((id REAL) (#) h),['a,c'])) / (integral (h,['a,c'])) by FUZZY_6:def 1
.= (integral (((id REAL) (#) h),['a,c'])) * (1 / (integral (h,['a,c']))) by XCMPLX_1:99 ;
hence centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c'])))) by A5; :: thesis: verum