let IT be RMembership_Func of C1,C2; ( IT = converse iff for x, y being object st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) )
A4:
dom h = [:C2,C1:]
by FUNCT_2:def 1;
thus
( IT = ~ h implies for x, y being object st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) )
( ( for x, y being object st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) ) implies IT = converse )proof
assume A5:
IT = ~ h
;
for x, y being object st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x)
let x,
y be
object ;
( [x,y] in [:C1,C2:] implies IT . (x,y) = h . (y,x) )
assume
[x,y] in [:C1,C2:]
;
IT . (x,y) = h . (y,x)
then
[y,x] in dom h
by A4, ZFMISC_1:88;
hence
IT . (
x,
y)
= h . (
y,
x)
by A5, FUNCT_4:def 2;
verum
end;
A6:
dom IT = [:C1,C2:]
by FUNCT_2:def 1;
A7:
for x being object holds
( x in dom IT iff ex y, z being object st
( x = [z,y] & [y,z] in dom h ) )
proof
let x be
object ;
( x in dom IT iff ex y, z being object st
( x = [z,y] & [y,z] in dom h ) )
thus
(
x in dom IT implies ex
y,
z being
object st
(
x = [z,y] &
[y,z] in dom h ) )
( ex y, z being object st
( x = [z,y] & [y,z] in dom h ) implies x in dom IT )proof
assume
x in dom IT
;
ex y, z being object st
( x = [z,y] & [y,z] in dom h )
then consider z,
y being
object such that A8:
z in C1
and A9:
y in C2
and A10:
x = [z,y]
by ZFMISC_1:def 2;
reconsider y =
y,
z =
z as
set by TARSKI:1;
take
y
;
ex z being object st
( x = [z,y] & [y,z] in dom h )
take
z
;
( x = [z,y] & [y,z] in dom h )
thus
(
x = [z,y] &
[y,z] in dom h )
by A4, A8, A9, A10, ZFMISC_1:def 2;
verum
end;
thus
( ex
y,
z being
object st
(
x = [z,y] &
[y,z] in dom h ) implies
x in dom IT )
by A6, ZFMISC_1:88;
verum
end;
assume
for x, y being object st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x)
; IT = converse
then
for y, z being object st [y,z] in dom h holds
IT . (z,y) = h . (y,z)
by ZFMISC_1:88;
hence
IT = converse
by A7, FUNCT_4:def 2; verum