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

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