let V be RealLinearSpace; :: thesis: for A being Subset of V holds Lin A = Lin (A \ {(0. V)})
let A be Subset of V; :: thesis: Lin A = Lin (A \ {(0. V)})

per cases ( not 0. V in A or 0. V in A ) ;

suppose not 0. V in A ; :: thesis: Lin A = Lin (A \ {(0. V)})

hence Lin A = Lin (A \ {(0. V)}) by ZFMISC_1:57; :: thesis: verum

end;

suppose A1: 0. V in A ; :: thesis: Lin A = Lin (A \ {(0. V)})

{(0. V)} = the carrier of ((0). V) by RLSUB_1:def 3;
then A2: Lin {(0. V)} = (0). V by RLVECT_3:18;
A = (A \ {(0. V)}) \/ {(0. V)} by A1, ZFMISC_1:116;
hence Lin A = (Lin (A \ {(0. V)})) + ((0). V) by A2, RLVECT_3:22
.= Lin (A \ {(0. V)}) by RLSUB_2:9 ;
:: thesis: verum

end;

end;