per cases ( v = 0. V or v <> 0. V ) ;
suppose B1: v = 0. V ; :: thesis: W + (Lin {v}) is free
reconsider Ws = (Omega). W as strict Subspace of V by ZMODUL01:42;
reconsider Lw = (Omega). (Lin {v}) as strict Subspace of V ;
W + (Lin {v}) = Ws + Lw by ZMODUL04:22
.= Ws + ((0). V) by B1, ThLin5
.= Ws by ZMODUL01:99 ;
hence W + (Lin {v}) is free ; :: thesis: verum
end;
suppose A1: v <> 0. V ; :: thesis: W + (Lin {v}) is free
per cases ( W /\ (Lin {v}) = (0). V or W /\ (Lin {v}) <> (0). V ) ;
suppose W /\ (Lin {v}) <> (0). V ; :: thesis: W + (Lin {v}) is free
hence W + (Lin {v}) is free by A1, LmSumModX; :: thesis: verum
end;
end;
end;
end;