theorem :: SETLIM_1:35

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 (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)