let o1, o2 be BinOp of (Union (G,RK)); :: thesis: ( ( for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
o1 . (w1,w2) = x \ y ) & ( for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
o2 . (w1,w2) = x \ y ) implies o1 = o2 )
assume A7: for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
o1 . (w1,w2) = x \ y ; :: thesis: ( ex w1, w2 being Element of Union (G,RK) ex x, y being Element of X st
( w1 = x & w2 = y & not o2 . (w1,w2) = x \ y ) or o1 = o2 )
assume A8: for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x & w2 = y holds
o2 . (w1,w2) = x \ y ; :: thesis: o1 = o2

now

let w1, w2 be Element of Union (G,RK); :: thesis: o1 . (w1,w2) = o2 . (w1,w2)
o1 . (w1,w2) = w1 \ w2 by A7;
hence o1 . (w1,w2) = o2 . (w1,w2) by A8; :: thesis: verum

end;

hence o1 = o2 by BINOP_1:2; :: thesis: verum