theorem :: SETLIM_1:36

for X being set
for A1, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)