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 (max (converse f),(converse g)) = [:C2,C1:] by FUNCT_2:def 1;
A2: 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
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
A6: [x,y] in [:C1,C2:] by A3, A4, ZFMISC_1:106;
(converse (max f,g)) . y,x = (max f,g) . x,y by A5, Def1
.= max (f . x,y),(g . x,y) by A6, FUZZY_1:def 5
.= max ((converse f) . y,x),(g . x,y) by A5, Def1
.= max ((converse f) . y,x),((converse g) . y,x) by A5, Def1
.= (max (converse f),(converse g)) . y,x by A5, FUZZY_1:def 5 ;
hence (converse (max f,g)) . c = (max (converse f),(converse g)) . c by A5; :: thesis: verum

end;

dom (converse (max f,g)) = [:C2,C1:] by FUNCT_2:def 1;
hence converse (max f,g) = max (converse f),(converse g) by A1, A2, PARTFUN1:34; :: thesis: verum