let n be Element of NAT ; :: thesis: for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f + g)
let a, b, c, d be Real; :: thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f + g)
let f, g be PartFunc of REAL,(REAL n); :: thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g implies ['c,d'] c= dom (f + g) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; :: thesis: ['c,d'] c= dom (f + g)
dom (f + g) = (dom f) /\ (dom g) by VALUED_2:def 45;
then ['a,b'] /\ ['a,b'] c= dom (f + g) by A2, XBOOLE_1:27;
hence ['c,d'] c= dom (f + g) by A1, Th2; :: thesis: verum