let f be FinSequence of NAT ; :: thesis: ( f <> {} implies UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra )
assume A1: f <> {} ; :: thesis: UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra
set U0 = UAStr(# {{}},(TrivialOps f) #);
A2: ( the charact of UAStr(# {{}},(TrivialOps f) #) is homogeneous & the charact of UAStr(# {{}},(TrivialOps f) #) is quasi_total & the charact of UAStr(# {{}},(TrivialOps f) #) is non-empty ) by Th9;
len the charact of UAStr(# {{}},(TrivialOps f) #) = len f by Def8;
then the charact of UAStr(# {{}},(TrivialOps f) #) <> {} by A1;
hence UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by A2, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; :: thesis: verum