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: [:C2,C1:] = dom (converse (1_minus f)) by FUNCT_2:def 1;
A2: 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
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;
(1_minus (converse f)) . y,x = 1 - ((converse f) . y,x) by A5, FUZZY_1:def 6
.= 1 - (f . x,y) by A5, Def1
.= (1_minus f) . x,y by A6, FUZZY_1:def 6
.= (converse (1_minus f)) . y,x by A5, Def1 ;
hence (1_minus (converse f)) . c = (converse (1_minus f)) . c by A5; :: thesis: verum

end;

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