:: deftheorem defines Trivial_Algebra PRALG_1:def 9 :
for f being non empty FinSequence of NAT holds Trivial_Algebra f = UAStr(# {{}},(TrivialOps f) #);