let f be PartFunc of REAL,REAL; :: thesis: for A being non empty closed_interval Subset of REAL st A c= dom f holds
( max+ (f || A) = max+ (f | A) & max- (f || A) = max- (f | A) )
let A be non empty closed_interval Subset of REAL; :: thesis: ( A c= dom f implies ( max+ (f || A) = max+ (f | A) & max- (f || A) = max- (f | A) ) )
assume A c= dom f ; :: thesis: ( max+ (f || A) = max+ (f | A) & max- (f || A) = max- (f | A) )
A1: ( dom (max+ (f || A)) = dom (f | A) & dom (f | A) = dom (max+ (f | A)) ) by RFUNCT_3:def 10;
for x being object st x in dom (max+ (f || A)) holds
(max+ (f || A)) . x = (max+ (f | A)) . x

proof

let x be object ; :: thesis: ( x in dom (max+ (f || A)) implies (max+ (f || A)) . x = (max+ (f | A)) . x )
assume A2: x in dom (max+ (f || A)) ; :: thesis: (max+ (f || A)) . x = (max+ (f | A)) . x
then (max+ (f || A)) . x = max+ ((f | A) . x) by RFUNCT_3:def 10;
hence (max+ (f || A)) . x = (max+ (f | A)) . x by A2, A1, RFUNCT_3:def 10; :: thesis: verum

end;

hence max+ (f || A) = max+ (f | A) by A1, FUNCT_1:2; :: thesis: max- (f || A) = max- (f | A)
A3: ( dom (max- (f || A)) = dom (f | A) & dom (f | A) = dom (max- (f | A)) ) by RFUNCT_3:def 11;
for x being object st x in dom (max- (f || A)) holds
(max- (f || A)) . x = (max- (f | A)) . x

proof

let x be object ; :: thesis: ( x in dom (max- (f || A)) implies (max- (f || A)) . x = (max- (f | A)) . x )
assume A4: x in dom (max- (f || A)) ; :: thesis: (max- (f || A)) . x = (max- (f | A)) . x
then (max- (f || A)) . x = max- ((f | A) . x) by RFUNCT_3:def 11;
hence (max- (f || A)) . x = (max- (f | A)) . x by A4, A3, RFUNCT_3:def 11; :: thesis: verum

end;

hence max- (f || A) = max- (f | A) by A3, FUNCT_1:2; :: thesis: verum