let o1, o2 be BinOp of (Subspaces V); :: thesis: ( ( for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 )

assume A2: for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o1 . (A1,A2) = W1 + W2 ; :: thesis: ( ex A1, A2 being Element of Subspaces V ex W1, W2 being Subspace of V st

( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 )

assume A3: for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o2 . (A1,A2) = W1 + W2 ; :: thesis: o1 = o2

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 )

assume A2: for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds

o1 . (A1,A2) = W1 + W2 ; :: thesis: ( ex A1, A2 being Element of Subspaces V ex W1, W2 being Subspace of V st

( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 )

assume A3: for A1, A2 being Element of Subspaces V

for W1, W2 being Subspace 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 Subspaces V & y in Subspaces V holds

o1 . (x,y) = o2 . (x,y)

hence
o1 = o2
by BINOP_1:1; :: thesis: verumo1 . (x,y) = o2 . (x,y)

let x, y be set ; :: thesis: ( x in Subspaces V & y in Subspaces V implies o1 . (x,y) = o2 . (x,y) )

assume A4: ( x in Subspaces V & y in Subspaces V ) ; :: thesis: o1 . (x,y) = o2 . (x,y)

then reconsider A = x, B = y as Element of Subspaces V ;

reconsider W1 = x, W2 = y as Subspace of V by A4, Def3;

o1 . (A,B) = W1 + W2 by A2;

hence o1 . (x,y) = o2 . (x,y) by A3; :: thesis: verum

end;assume A4: ( x in Subspaces V & y in Subspaces V ) ; :: thesis: o1 . (x,y) = o2 . (x,y)

then reconsider A = x, B = y as Element of Subspaces V ;

reconsider W1 = x, W2 = y as Subspace of V by A4, Def3;

o1 . (A,B) = W1 + W2 by A2;

hence o1 . (x,y) = o2 . (x,y) by A3; :: thesis: verum