let f, g be Fuzzy_Negation; :: thesis: max (f,g) = (maxfuncreal [.0,1.]) . (f,g)
set A = [.0,1.];
set fg = max (f,g);
set mfg = (maxfuncreal [.0,1.]) . (f,g);
B1: dom (max (f,g)) = [.0,1.] by FUNCT_2:def 1;
AC: ( f in Funcs ([.0,1.],REAL) & g in Funcs ([.0,1.],REAL) & Funcs ([.0,1.],REAL) <> {} ) by LemmaFunc2;
(maxfuncreal [.0,1.]) . (f,g) in Funcs ([.0,1.],REAL) by AC, BINOP_1:17;
then consider f1 being Function such that
C1: ( (maxfuncreal [.0,1.]) . (f,g) = f1 & dom f1 = [.0,1.] & rng f1 c= REAL ) by FUNCT_2:def 2;
for x being object st x in [.0,1.] holds
(max (f,g)) . x = ((maxfuncreal [.0,1.]) . (f,g)) . x

proof

let x be object ; :: thesis: ( x in [.0,1.] implies (max (f,g)) . x = ((maxfuncreal [.0,1.]) . (f,g)) . x )
assume D0: x in [.0,1.] ; :: thesis: (max (f,g)) . x = ((maxfuncreal [.0,1.]) . (f,g)) . x
consider f2, g2 being Function of [.0,1.],REAL such that
D1: ( f2 = f & g2 = g & max (f,g) = max (f2,g2) ) by MaxFuz;
( dom f = [.0,1.] & rng f c= REAL & dom g = [.0,1.] & rng g c= REAL ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider fA = f, gA = g as Element of Funcs ([.0,1.],REAL) by FUNCT_2:def 2;
dom (maxreal .: (fA,gA)) = [.0,1.] by FUNCT_2:def 1;
then (maxreal .: (fA,gA)) . x = maxreal . ((fA . x),(gA . x)) by D0, FUNCOP_1:22
.= max ((fA . x),(gA . x)) by REAL_LAT:def 2
.= (max (f,g)) . x by D1, D0, COUSIN2:def 2 ;
hence (max (f,g)) . x = ((maxfuncreal [.0,1.]) . (f,g)) . x by REAL_LAT:def 4; :: thesis: verum

end;

hence max (f,g) = (maxfuncreal [.0,1.]) . (f,g) by C1, B1, FUNCT_1:2; :: thesis: verum