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

now

let n be Element of NAT ; :: thesis: Un . n is locally_finite
Un . n is discrete by A1, Def2;
hence Un . n is locally_finite by Th11; :: thesis: verum

end;

hence Un is sigma_locally_finite by Def3; :: thesis: verum

end;