let X be set ; :: thesis: for O1, O2 being Operation of X st ( for x being Element of X holds x . O1 = x . O2 ) holds

O1 = O2

let O1, O2 be Operation of X; :: thesis: ( ( for x being Element of X holds x . O1 = x . O2 ) implies O1 = O2 )

assume A1: for x being Element of X holds x . O1 = x . O2 ; :: thesis: O1 = O2

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in O1 or [a,b] in O2 ) & ( not [a,b] in O2 or [a,b] in O1 ) )

thus ( [a,b] in O1 implies [a,b] in O2 ) :: thesis: ( not [a,b] in O2 or [a,b] in O1 )

then A4: ( a in X & b in X ) by ZFMISC_1:87;

reconsider a = a, b = b as Element of X by A3, ZFMISC_1:87;

reconsider L = {a} as Subset of X by A4, ZFMISC_1:31;

b in a . O2 by A3, RELAT_1:169;

then b in a . O1 by A1;

hence [a,b] in O1 by RELAT_1:169; :: thesis: verum

O1 = O2

let O1, O2 be Operation of X; :: thesis: ( ( for x being Element of X holds x . O1 = x . O2 ) implies O1 = O2 )

assume A1: for x being Element of X holds x . O1 = x . O2 ; :: thesis: O1 = O2

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in O1 or [a,b] in O2 ) & ( not [a,b] in O2 or [a,b] in O1 ) )

thus ( [a,b] in O1 implies [a,b] in O2 ) :: thesis: ( not [a,b] in O2 or [a,b] in O1 )

proof

assume A3:
[a,b] in O2
; :: thesis: [a,b] in O1
assume A2:
[a,b] in O1
; :: thesis: [a,b] in O2

reconsider a = a, b = b as Element of X by A2, ZFMISC_1:87;

b in a . O1 by A2, RELAT_1:169;

then b in a . O2 by A1;

hence [a,b] in O2 by RELAT_1:169; :: thesis: verum

end;reconsider a = a, b = b as Element of X by A2, ZFMISC_1:87;

b in a . O1 by A2, RELAT_1:169;

then b in a . O2 by A1;

hence [a,b] in O2 by RELAT_1:169; :: thesis: verum

then A4: ( a in X & b in X ) by ZFMISC_1:87;

reconsider a = a, b = b as Element of X by A3, ZFMISC_1:87;

reconsider L = {a} as Subset of X by A4, ZFMISC_1:31;

b in a . O2 by A3, RELAT_1:169;

then b in a . O1 by A1;

hence [a,b] in O1 by RELAT_1:169; :: thesis: verum