per cases ( v = 0. V or v <> 0. V ) ;

suppose v = 0. V ; :: thesis: Lin {v} is free

then Lin {v} = (0). V by ThLin5;
hence Lin {v} is free ; :: thesis: verum

end;

suppose v <> 0. V ; :: thesis: Lin {v} is free

then not v is torsion by defTorsionFree;
hence Lin {v} is free by ThnTV4; :: thesis: verum

end;

end;