:: deftheorem defines trivial REALALG2:def 4 :
for R being ZeroStr
for f being the carrier of b₁ -valued Function holds
( f is trivial iff for i being object st i in dom f holds
f . i = 0. R );