for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)