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 A4: 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 A5: 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 A4;
hence o1 . w1,w2 = o2 . w1,w2 by A5; :: thesis: verum

end;

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