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']))) * ((integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) 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']))) * ((integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c']))) )
assume that
A1: ( a <= b & b <= c & f is continuous & g is continuous ) and
A2: h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) and
A3: ( integral (f,['a,b']) <> 0 & integral (g,['b,c']) <> 0 ) and
A4: f . b = g . b ; :: thesis: centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * ((integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c'])))
thus 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 FUZZY_8:17, A1, A2, A3, A4
.= (1 / (integral (h,['a,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
.= (1 / (integral (h,['a,c']))) * ((((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
.= (1 / (integral (h,['a,c']))) * ((integral (((id REAL) (#) f),['a,b'])) + (((integral (((id REAL) (#) g),['b,c'])) / (integral (g,['b,c']))) * (integral (g,['b,c'])))) by XCMPLX_1:87, A3
.= (1 / (integral (h,['a,c']))) * ((integral (((id REAL) (#) f),['a,b'])) + (integral (((id REAL) (#) g),['b,c']))) by XCMPLX_1:87, A3 ; :: thesis: verum