let n be Element of NAT ; 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; 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); ( 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 )
; ['c,d'] c= dom (f - g)
dom (f - g) = (dom f) /\ (dom g)
by VALUED_2:def 46;
then
['a,b'] /\ ['a,b'] c= dom (f - g)
by A2, XBOOLE_1:27;
hence
['c,d'] c= dom (f - g)
by A1, Th2; verum