let o1, o2 be BinOp of (Submodules V); ( ( 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
; ( 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
; o1 = o2
now 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 ;
( 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
;
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;
verum end;
hence
o1 = o2
by BINOP_1:1; verum