let x, y be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: ( not x in field ((f * R) * (f ")) or not y in field ((f * R) * (f ")) or not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y )

assume that

x in field ((f * R) * (f ")) and

y in field ((f * R) * (f ")) ; :: thesis: ( not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y )

assume that

A1: [x,y] in (f * R) * (f ") and

A2: [y,x] in (f * R) * (f ") ; :: thesis: x = y

A3: ( x in dom f & y in dom f ) by A1, Th6;

A4: R is_antisymmetric_in field R by RELAT_2:def 12;

A5: [(f . y),(f . x)] in R by A2, Th6;

A6: [(f . x),(f . y)] in R by A1, Th6;

then ( f . x in field R & f . y in field R ) by RELAT_1:15;

then f . x = f . y by A6, A5, A4;

hence x = y by A3, FUNCT_1:def 4; :: thesis: verum

assume that

x in field ((f * R) * (f ")) and

y in field ((f * R) * (f ")) ; :: thesis: ( not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y )

assume that

A1: [x,y] in (f * R) * (f ") and

A2: [y,x] in (f * R) * (f ") ; :: thesis: x = y

A3: ( x in dom f & y in dom f ) by A1, Th6;

A4: R is_antisymmetric_in field R by RELAT_2:def 12;

A5: [(f . y),(f . x)] in R by A2, Th6;

A6: [(f . x),(f . y)] in R by A1, Th6;

then ( f . x in field R & f . y in field R ) by RELAT_1:15;

then f . x = f . y by A6, A5, A4;

hence x = y by A3, FUNCT_1:def 4; :: thesis: verum