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;