let o1, o2 be BinOp of (Cosets N); :: thesis: ( ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o2 . (W1,W2) = A1 * A2 ) implies o1 = o2 )
assume A2: for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o1 . (W1,W2) = A1 * A2 ; :: thesis: ( ex W1, W2 being Element of Cosets N ex A1, A2 being Subset of G st
( W1 = A1 & W2 = A2 & not o2 . (W1,W2) = A1 * A2 ) or o1 = o2 )
assume A3: for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o2 . (W1,W2) = A1 * A2 ; :: thesis: o1 = o2

now

let x, y be set ; :: thesis: ( x in Cosets N & y in Cosets N implies o1 . (x,y) = o2 . (x,y) )
assume A4: ( x in Cosets N & y in Cosets N ) ; :: thesis: o1 . (x,y) = o2 . (x,y)
then reconsider W = x, V = y as Element of Cosets N ;
reconsider A1 = x, A2 = y as Subset of G by A4;
o1 . (W,V) = A1 * A2 by A2;
hence o1 . (x,y) = o2 . (x,y) by A3; :: thesis: verum

end;

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