consider A being non empty set ;
consider a being Element of A;
reconsider w = (<*> A) .--> a as Element of PFuncs ((A *),A) by MARGREL1:55;
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 non-empty & the charact of UAStr(# A,<*w*> #) <> {} ) by MARGREL1:56;
( the charact of UAStr(# A,<*w*> #) is quasi_total & the charact of UAStr(# A,<*w*> #) is homogeneous ) by MARGREL1: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