let f, g be Function of REAL,REAL; :: thesis: max (f,g) = (1 / 2) (#) ((f + g) + (abs (f - g)))
D1: REAL = dom ((1 / 2) (#) ((f + g) + (abs (f - g)))) by FUNCT_2:52;
for x being object st x in dom (max (f,g)) holds
(max (f,g)) . x = ((1 / 2) (#) ((f + g) + (abs (f - g)))) . x

proof

let x be object ; :: thesis: ( x in dom (max (f,g)) implies (max (f,g)) . x = ((1 / 2) (#) ((f + g) + (abs (f - g)))) . x )
assume A0: x in dom (max (f,g)) ; :: thesis: (max (f,g)) . x = ((1 / 2) (#) ((f + g) + (abs (f - g)))) . x
then A1: x in REAL ;
then A2: x in dom ((f + g) + (abs (f - g))) by FUNCT_2:52;
A3: x in dom (f - g) by A1, FUNCT_2:52;
A4: x in dom (f + g) by A1, FUNCT_2:52;
reconsider x = x as Element of REAL by A0;
((1 / 2) (#) ((f + g) + (abs (f - g)))) . x = (1 / 2) * (((f + g) + (abs (f - g))) . x) by VALUED_1:6
.= (1 / 2) * (((f + g) . x) + ((abs (f - g)) . x)) by VALUED_1:def 1, A2
.= (1 / 2) * (((f + g) . x) + |.((f - g) . x).|) by VALUED_1:18
.= (1 / 2) * (((f + g) . x) + |.((f . x) - (g . x)).|) by VALUED_1:13, A3
.= (1 / 2) * (((f . x) + (g . x)) + |.((f . x) - (g . x)).|) by VALUED_1:def 1, A4
.= (((f . x) + (g . x)) + |.((f . x) - (g . x)).|) / 2
.= max ((f . x),(g . x)) by COMPLEX1:74 ;
hence (max (f,g)) . x = ((1 / 2) (#) ((f + g) + (abs (f - g)))) . x by COUSIN2:def 2; :: thesis: verum

end;

hence max (f,g) = (1 / 2) (#) ((f + g) + (abs (f - g))) by FUNCT_1:2, D1, FUNCT_2:52; :: thesis: verum