:: deftheorem defines FreeUnivAlgZAO FREEALG:def 18 :
for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);