theorem :: SETLIM_2:49

for n being Nat
for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n