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 object such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def 2;
reconsider y = y, x = x as set by TARSKI:1;
A6: [x,y] in [:C1,C2:] by A3, A4, ZFMISC_1:87;
(1_minus (converse f)) . (y,x) = 1 - ((converse f) . (y,x)) by A5, FUZZY_1:def 5
.= 1 - (f . (x,y)) by A5, Def1
.= (1_minus f) . (x,y) by A6, FUZZY_1:def 5
.= (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:5; :: thesis: verum