consider D being non empty set , c being PFuncFinSequence of D;
take UAStr(# D,c #) ; :: thesis: ( not UAStr(# D,c #) is empty & UAStr(# D,c #) is strict )
thus not the carrier of UAStr(# D,c #) is empty ; :: according to STRUCT_0:def 1 :: thesis: UAStr(# D,c #) is strict
thus UAStr(# D,c #) is strict ; :: thesis: verum