theorem FRdsY: :: ZMODUL04:33

for V being free Z_Module
for I being Basis of V
for v being Vector of V st v in I holds
V is_the_direct_sum_of Lin (I \ {v}), Lin {v}