let f be Function of REAL,REAL; :: thesis: max+ f = max ((AffineMap (0,0)),f)
dom f = REAL by FUNCT_2:def 1;
then B7: dom (max+ f) = REAL by RFUNCT_3:def 10;
then A2: dom (max+ f) = dom (max ((AffineMap (0,0)),f)) by FUNCT_2:def 1;
set F = max ((AffineMap (0,0)),f);
for x being object st x in dom (max ((AffineMap (0,0)),f)) holds
(max ((AffineMap (0,0)),f)) . x = (max+ f) . x

proof

let x be object ; :: thesis: ( x in dom (max ((AffineMap (0,0)),f)) implies (max ((AffineMap (0,0)),f)) . x = (max+ f) . x )
assume x in dom (max ((AffineMap (0,0)),f)) ; :: thesis: (max ((AffineMap (0,0)),f)) . x = (max+ f) . x
then reconsider x = x as Element of REAL ;
(max+ f) . x = max+ (f . x) by RFUNCT_3:def 10, B7
.= max ((f . x),((0 * x) + 0)) by RFUNCT_3:def 1
.= max ((f . x),((AffineMap (0,0)) . x)) by FCONT_1:def 4
.= (max (f,(AffineMap (0,0)))) . x by COUSIN2:def 2 ;
hence (max ((AffineMap (0,0)),f)) . x = (max+ f) . x ; :: thesis: verum

end;

hence max ((AffineMap (0,0)),f) = max+ f by FUNCT_1:2, A2; :: thesis: verum