:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Partial_Diff_Union A1 iff ( b₃ . 0 = A1 . 0 & ( for n being Nat holds b₃ . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) );