thus ex Un being FamilySequence of T st Un is sigma_locally_finite :: thesis: verum

proof

consider Un being FamilySequence of T such that
A1: Un is sigma_discrete by Lm5;
take Un ; :: thesis: Un is sigma_locally_finite
for n being Element of NAT holds Un . n is locally_finite by Th11, A1;
hence Un is sigma_locally_finite ; :: thesis: verum

end;