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:106;
hence (converse f) . y,x = f . x,y by Def1; :: thesis: verum