let X be set ; :: thesis: for S being non empty right_zeroed addLoopStr
for p, q being Series of X,S
for V being set st vars p c= V & vars q c= V holds
vars (p + q) c= V
let S be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Series of X,S
for V being set st vars p c= V & vars q c= V holds
vars (p + q) c= V
let p, q be Series of X,S; :: thesis: for V being set st vars p c= V & vars q c= V holds
vars (p + q) c= V
let V be set ; :: thesis: ( vars p c= V & vars q c= V implies vars (p + q) c= V )
assume ( vars p c= V & vars q c= V ) ; :: thesis: vars (p + q) c= V
then ( vars (p + q) c= (vars p) \/ (vars q) & (vars p) \/ (vars q) c= V ) by Th41, XBOOLE_1:8;
hence vars (p + q) c= V ; :: thesis: verum