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

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