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;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