let o1, o2 be BinOp of (Submodules V); :: thesis: ( ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ; :: thesis: ( ex A1, A2 being Element of Submodules V ex W1, W2 being Submodule of V st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 /\ W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ; :: thesis: o1 = o2

now :: thesis: for x, y being set st x in Submodules V & y in Submodules V holds
o1 . (x,y) = o2 . (x,y)

let x, y be set ; :: thesis: ( x in Submodules V & y in Submodules V implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Submodules V and
A7: y in Submodules V ; :: thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Submodules V by A6, A7;
consider W1 being strict Submodule of V such that
A8: W1 = x by A6, Def3;
consider W2 being strict Submodule of V such that
A9: W2 = y by A7, Def3;
o1 . (A,B) = W1 /\ W2 by A4, A8, A9;
hence o1 . (x,y) = o2 . (x,y) by A5, A8, A9; :: thesis: verum

end;

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