let C1, C2 be non empty set ; 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; 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:];
( c in [:C2,C1:] implies (1_minus (converse f)) . c = (converse (1_minus f)) . c )
assume
c in [:C2,C1:]
;
(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;
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; verum