let V be free Z_Module; :: thesis: for I being Basis of V
for v being Vector of V st v in I holds
( Lin (I \ {v}) is free & Lin {v} is free )
let I be Basis of V; :: thesis: for v being Vector of V st v in I holds
( Lin (I \ {v}) is free & Lin {v} is free )
let v be Vector of V; :: thesis: ( v in I implies ( Lin (I \ {v}) is free & Lin {v} is free ) )
assume A1: v in I ; :: thesis: ( Lin (I \ {v}) is free & Lin {v} is free )
A2: I is linearly-independent by VECTSP_7:def 3;
then I \ {v} is linearly-independent by XBOOLE_1:36, ZMODUL02:56;
hence Lin (I \ {v}) is free ; :: thesis: Lin {v} is free
{v} is linearly-independent by A1, A2, ZFMISC_1:31, ZMODUL02:56;
hence Lin {v} is free ; :: thesis: verum