let C1, C2 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2 holds 1_minus (converse f) = converse (1_minus f)
let f be RMembership_Func of C1,C2; :: thesis: 1_minus (converse f) = converse (1_minus f)
A1: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds
(1_minus (converse f)) . c = (converse (1_minus f)) . c

proof

let c be Element of [:C2,C1:]; :: thesis: ( c in [:C2,C1:] implies (1_minus (converse f)) . c = (converse (1_minus f)) . c )
assume c in [:C2,C1:] ; :: thesis: (1_minus (converse f)) . c = (converse (1_minus f)) . 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;
(1_minus (converse f)) . y,x = 1 - ((converse f) . y,x) by A2, FUZZY_1:def 6
.= 1 - (f . x,y) by A2, Def1
.= (1_minus f) . x,y by A3, FUZZY_1:def 6
.= (converse (1_minus f)) . y,x by A2, Def1 ;
hence (1_minus (converse f)) . c = (converse (1_minus f)) . c by A2; :: thesis: verum

end;

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