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