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

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

end;