let V be RealLinearSpace; :: thesis: for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
let A be Subset of V; :: thesis: Lin (A \/ {(0. V)}) = Lin A
{(0. V)} = the carrier of ((0). V) by RLSUB_1:def 3;
then Lin {(0. V)} = (0). V by RLVECT_3:18;
hence Lin (A \/ {(0. V)}) = (Lin A) + ((0). V) by RLVECT_3:22
.= Lin A by RLSUB_2:9 ;
:: thesis: verum