set A = the non empty set ;
set a = the Element of the non empty set ;
reconsider w = (<*> the non empty set ) .--> the Element of the non empty set as Element of PFuncs (( the non empty set *), the non empty set ) by MARGREL1:19;
set U1 = UAStr(# the non empty set ,<*w*> #);
take UAStr(# the non empty set ,<*w*> #) ; :: thesis: ( UAStr(# the non empty set ,<*w*> #) is quasi_total & UAStr(# the non empty set ,<*w*> #) is partial & UAStr(# the non empty set ,<*w*> #) is non-empty & UAStr(# the non empty set ,<*w*> #) is strict & not UAStr(# the non empty set ,<*w*> #) is empty )
A1: ( the charact of UAStr(# the non empty set ,<*w*> #) is non-empty & the charact of UAStr(# the non empty set ,<*w*> #) <> {} ) by MARGREL1:20;
( the charact of UAStr(# the non empty set ,<*w*> #) is quasi_total & the charact of UAStr(# the non empty set ,<*w*> #) is homogeneous ) by MARGREL1:20;
hence ( UAStr(# the non empty set ,<*w*> #) is quasi_total & UAStr(# the non empty set ,<*w*> #) is partial & UAStr(# the non empty set ,<*w*> #) is non-empty & UAStr(# the non empty set ,<*w*> #) is strict & not UAStr(# the non empty set ,<*w*> #) is empty ) by A1; :: thesis: verum