let f, g be Fuzzy_Negation; for ff, gg being Membership_Func of [.0,1.] st f = ff & g = gg holds
max (f,g) = max (ff,gg)
let ff, gg be Membership_Func of [.0,1.]; ( f = ff & g = gg implies max (f,g) = max (ff,gg) )
assume A1:
( f = ff & g = gg )
; max (f,g) = max (ff,gg)
consider f1, g1 being Function of [.0,1.],REAL such that
A2:
( f1 = f & g1 = g & max (f,g) = max (f1,g1) )
by MaxFuz;
reconsider ff1 = f1, gg1 = g1 as Membership_Func of [.0,1.] by A2;
for c being Element of [.0,1.] holds (max (ff1,gg1)) . c = max ((ff1 . c),(gg1 . c))
by FUZZY_1:def 4;
hence
max (f,g) = max (ff,gg)
by A1, A2, COUSIN2:def 2; verum