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 Th10;
len the charact of UAStr(# {{} },(TrivialOps f) #) = len f by Def8;
then len the charact of UAStr(# {{} },(TrivialOps f) #) <> 0 by A1;
then the charact of UAStr(# {{} },(TrivialOps f) #) <> {} ;
hence UAStr(# {{} },(TrivialOps f) #) is strict Universal_Algebra by A2, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum