:: deftheorem Def5 defines GoCross_Partial_Union FINANCE2:def 3 :
for k being Nat
for pm being Element of REAL
for b₃ being SetSequence of REAL holds
( b₃ = GoCross_Partial_Union (pm,k) iff ( b₃ . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) ) );