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

now

let c be Element of C; :: thesis: (@ ((C,f @ ) "\/" (C,g @ ))) . c = max (f . c),(g . c)
( ( for c being Element of C holds (C --> (RealPoset [.0 ,1.])) . c is sup-Semilattice ) & (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, Th12
.= max (f . c),(g . c) ;
:: thesis: verum

end;

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