:: deftheorem Def1 defines non-trivial NDIFF_5:def 1 :
for G being RealNormSpace-Sequence holds
( G is non-trivial iff for j being Element of dom G holds not G . j is trivial );