let x, y be object ; :: thesis: ( x indom f & y indom t implies ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) ) ) assume that A3:
x indom f
and A4:
y indom t
; :: thesis: ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) ) reconsider y1 = y as Element of D byA4; reconsider x1 = x as Element of C byA3; thus
( f . x = y implies t . y = x )
:: thesis: ( t . y = x implies f . x = y )