let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 holds converse (max f,g) = max (converse f),(converse g)
let f, g be RMembership_Func of C1,C2; :: thesis: converse (max f,g) = max (converse f),(converse g)
A1: ( dom (converse (max f,g)) = [:C2,C1:] & dom (max (converse f),(converse g)) = [:C2,C1:] ) by FUNCT_2:def 1;
for c being Element of [:C2,C1:] st c in [:C2,C1:] holds
(converse (max f,g)) . c = (max (converse f),(converse g)) . c

proof

let c be Element of [:C2,C1:]; :: thesis: ( c in [:C2,C1:] implies (converse (max f,g)) . c = (max (converse f),(converse g)) . c )
assume c in [:C2,C1:] ; :: thesis: (converse (max f,g)) . c = (max (converse f),(converse g)) . c
consider y, x being set such that
A2: ( y in C2 & x in C1 & c = [y,x] ) by ZFMISC_1:def 2;
A3: [x,y] in [:C1,C2:] by A2, ZFMISC_1:106;
(converse (max f,g)) . y,x = (max f,g) . x,y by A2, Def1
.= max (f . x,y),(g . x,y) by A3, FUZZY_1:def 5
.= max ((converse f) . y,x),(g . x,y) by A2, Def1
.= max ((converse f) . y,x),((converse g) . y,x) by A2, Def1
.= (max (converse f),(converse g)) . y,x by A2, FUZZY_1:def 5 ;
hence (converse (max f,g)) . c = (max (converse f),(converse g)) . c by A2; :: thesis: verum

end;

hence converse (max f,g) = max (converse f),(converse g) by A1, PARTFUN1:34; :: thesis: verum