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

now

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

end;

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