let f, g be Fuzzy_Negation; :: thesis: min (f,g) = (minfuncreal [.0,1.]) . (f,g)
set A = [.0,1.];
set fg = min (f,g);
set mfg = (minfuncreal [.0,1.]) . (f,g);
B1: dom (min (f,g)) = [.0,1.] by FUNCT_2:def 1;
( f in Funcs ([.0,1.],REAL) & g in Funcs ([.0,1.],REAL) & Funcs ([.0,1.],REAL) <> {} ) by LemmaFunc2;
then (minfuncreal [.0,1.]) . (f,g) in Funcs ([.0,1.],REAL) by BINOP_1:17;
then consider f1 being Function such that
C1: ( (minfuncreal [.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
(min (f,g)) . x = ((minfuncreal [.0,1.]) . (f,g)) . x

proof

let x be object ; :: thesis: ( x in [.0,1.] implies (min (f,g)) . x = ((minfuncreal [.0,1.]) . (f,g)) . x )
assume D0: x in [.0,1.] ; :: thesis: (min (f,g)) . x = ((minfuncreal [.0,1.]) . (f,g)) . x
consider f2, g2 being Function of [.0,1.],REAL such that
D1: ( f2 = f & g2 = g & min (f,g) = min (f2,g2) ) by MinFuz;
( 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 (minreal .: (fA,gA)) = [.0,1.] by FUNCT_2:def 1;
then (minreal .: (fA,gA)) . x = minreal . ((fA . x),(gA . x)) by D0, FUNCOP_1:22
.= min ((fA . x),(gA . x)) by REAL_LAT:def 1
.= (min (f,g)) . x by D1, D0, COUSIN2:def 1 ;
hence (min (f,g)) . x = ((minfuncreal [.0,1.]) . (f,g)) . x by REAL_LAT:def 5; :: thesis: verum

end;

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