theorem XXTh1: :: ZMODUL04:17

for V being free Z_Module
for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds
A is linearly-dependent