let F be NAT -defined the Instructions of S -valued finite Function; :: thesis: ( F is really-closed & F is initial & not F is empty implies F is paraclosed )
assume A1: F is really-closed ; :: thesis: ( not F is initial or F is empty or F is paraclosed )
assume ( F is initial & not F is empty ) ; :: thesis: F is paraclosed
then 0 in dom F by AFINSQ_1:65;
hence F is paraclosed by A1, Th44; :: thesis: verum