theorem :: FUZZY_6:38

for a, b, c being Real
for f, g, h being Function of REAL,REAL st a <= c & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b holds
( ( b <= a implies h | [.a,c.] = g | [.a,c.] ) & ( c <= b implies h | [.a,c.] = f | [.a,c.] ) )