let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds min f,g = (C,f @ ) "/\" (C,g @ )
let f, g be Membership_Func of C; :: thesis: min f,g = (C,f @ ) "/\" (C,g @ )
A1: (RealPoset [.0 ,1.]) |^ C = product (C --> (RealPoset [.0 ,1.])) by YELLOW_1:def 5;
set fg = (C,f @ ) "/\" (C,g @ );
set R = RealPoset [.0 ,1.];
set J = C --> (RealPoset [.0 ,1.]);

now

let c be Element of C; :: thesis: (@ ((C,f @ ) "/\" (C,g @ ))) . c = min (f . c),(g . c)
A2: for c being Element of C holds (C --> (RealPoset [.0 ,1.])) . c is Semilattice by FUNCOP_1:13;
(C --> (RealPoset [.0 ,1.])) . c = RealPoset [.0 ,1.] by FUNCOP_1:13;
hence (@ ((C,f @ ) "/\" (C,g @ ))) . c = ((C,f @ ) . c) "/\" ((C,g @ ) . c) by A1, A2, Th11
.= min (f . c),(g . c) ;
:: thesis: verum

end;

hence min f,g = (C,f @ ) "/\" (C,g @ ) by FUZZY_1:def 4; :: thesis: verum