for X being set
for A1 being SetSequence of X st A1 is non-descending holds
( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )