:: deftheorem Def6 defines GoCross_Union FINANCE2:def 4 :
for pm being Element of REAL
for b₂ being SetSequence of REAL holds
( b₂ = GoCross_Union pm iff ( b₂ . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) ) );