take G = <* the non trivial RealNormSpace*>; :: thesis: G is non-trivial
let j be Element of dom G; :: according to NDIFF_5:def 1 :: thesis: not G . j is trivial
dom G = Seg 1 by FINSEQ_1:38;
then j = 1 by FINSEQ_1:2, TARSKI:def 1;
hence not G . j is trivial by FINSEQ_1:40; :: thesis: verum