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)})

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 )
;

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;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