let a, b, c, d be real number ; :: thesis: for f, g being PartFunc of REAL ,REAL st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
( integral (f + g),c,d = (integral f,c,d) + (integral g,c,d) & integral (f - g),c,d = (integral f,c,d) - (integral g,c,d) )
let f, g be PartFunc of REAL ,REAL ; :: thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies ( integral (f + g),c,d = (integral f,c,d) + (integral g,c,d) & integral (f - g),c,d = (integral f,c,d) - (integral g,c,d) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ( integral (f + g),c,d = (integral f,c,d) + (integral g,c,d) & integral (f - g),c,d = (integral f,c,d) - (integral g,c,d) )

now

assume A2: not c <= d ; :: thesis: ( integral (f + g),c,d = (integral f,c,d) + (integral g,c,d) & integral (f - g),c,d = (integral f,c,d) - (integral g,c,d) )
then A3: integral f,c,d = - (integral f,['d,c']) by INTEGRA5:def 5;
A4: integral g,c,d = - (integral g,['d,c']) by A2, INTEGRA5:def 5;
integral (f + g),c,d = - (integral (f + g),['d,c']) by A2, INTEGRA5:def 5;
hence integral (f + g),c,d = - (integral (f + g),d,c) by A2, INTEGRA5:def 5
.= - ((integral f,d,c) + (integral g,d,c)) by A1, A2, Lm11
.= (- (integral f,d,c)) - (integral g,d,c)
.= (integral f,c,d) - (integral g,d,c) by A2, A3, INTEGRA5:def 5
.= (integral f,c,d) + (integral g,c,d) by A2, A4, INTEGRA5:def 5 ;
:: thesis: integral (f - g),c,d = (integral f,c,d) - (integral g,c,d)
integral (f - g),c,d = - (integral (f - g),['d,c']) by A2, INTEGRA5:def 5;
hence integral (f - g),c,d = - (integral (f - g),d,c) by A2, INTEGRA5:def 5
.= - ((integral f,d,c) - (integral g,d,c)) by A1, A2, Lm11
.= - ((integral f,d,c) + (integral g,c,d)) by A2, A4, INTEGRA5:def 5
.= (- (integral f,d,c)) - (integral g,c,d)
.= (integral f,c,d) - (integral g,c,d) by A2, A3, INTEGRA5:def 5 ;
:: thesis: verum

end;

hence ( integral (f + g),c,d = (integral f,c,d) + (integral g,c,d) & integral (f - g),c,d = (integral f,c,d) - (integral g,c,d) ) by A1, Lm11; :: thesis: verum