consider A being non empty set ;
consider a being Element of A;
reconsider w = (<*> A) .--> a as Element of PFuncs (A * ),A by Th3;
set U1 = UAStr(# A,<*w*> #);
take UAStr(# A,<*w*> #) ; :: thesis: ( UAStr(# A,<*w*> #) is quasi_total & UAStr(# A,<*w*> #) is partial & UAStr(# A,<*w*> #) is non-empty & UAStr(# A,<*w*> #) is strict & not UAStr(# A,<*w*> #) is empty )
A1: ( the charact of UAStr(# A,<*w*> #) is quasi_total & the charact of UAStr(# A,<*w*> #) is homogeneous & the charact of UAStr(# A,<*w*> #) is non-empty ) by Th4;
the charact of UAStr(# A,<*w*> #) <> {} by CARD_1:47, FINSEQ_1:56;
hence ( UAStr(# A,<*w*> #) is quasi_total & UAStr(# A,<*w*> #) is partial & UAStr(# A,<*w*> #) is non-empty & UAStr(# A,<*w*> #) is strict & not UAStr(# A,<*w*> #) is empty ) by A1, Def7, Def8, Def9; :: thesis: verum