let X, Y be non empty set ; :: thesis: for x being Element of X
for y being Element of Y
for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
let x be Element of X; :: thesis: for y being Element of Y
for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
let y be Element of Y; :: thesis: for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
let f be RMembership_Func of X,Y; :: thesis: (converse f) . (y,x) = f . (x,y)
[y,x] in [:Y,X:] by ZFMISC_1:87;
hence (converse f) . (y,x) = f . (x,y) by Def1; :: thesis: verum