theorem Th13: :: SYMSP_1:13

for F being Field
for S being SymSp of F
for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_