let C1, C2 be non empty set ; for f, g being RMembership_Func of C1,C2 holds converse (min (f,g)) = min ((converse f),(converse g))
let f, g be RMembership_Func of C1,C2; converse (min (f,g)) = min ((converse f),(converse g))
A1:
dom (min ((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 (min (f,g))) . c = (min ((converse f),(converse g))) . c
proof
let c be
Element of
[:C2,C1:];
( c in [:C2,C1:] implies (converse (min (f,g))) . c = (min ((converse f),(converse g))) . c )
assume
c in [:C2,C1:]
;
(converse (min (f,g))) . c = (min ((converse f),(converse g))) . 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;
(converse (min (f,g))) . (
y,
x) =
(min (f,g)) . (
x,
y)
by A5, Def1
.=
min (
(f . (x,y)),
(g . (x,y)))
by A6, FUZZY_1:def 3
.=
min (
((converse f) . (y,x)),
(g . (x,y)))
by A5, Def1
.=
min (
((converse f) . (y,x)),
((converse g) . (y,x)))
by A5, Def1
;
hence
(converse (min (f,g))) . c = (min ((converse f),(converse g))) . c
by A5, FUZZY_1:def 3;
verum
end;
dom (converse (min (f,g))) = [:C2,C1:]
by FUNCT_2:def 1;
hence
converse (min (f,g)) = min ((converse f),(converse g))
by A1, A2, PARTFUN1:5; verum