:: deftheorem Def7 defines Union_Shift_Seq BOR_CANT:def 7 :
for X being set
for A, b₃ being SetSequence of X holds
( b₃ = Union_Shift_Seq A iff for n being Nat holds b₃ . n = Union (A ^\ n) );