let f be CR_Sequence; :: thesis: not f is multiplicative-trivial

now :: thesis: for i being Nat st i in dom f holds
f . i <> 0

let i be Nat; :: thesis: ( i in dom f implies f . i <> 0 )
assume i in dom f ; :: thesis: f . i <> 0
then f . i in rng f by FUNCT_1:3;
hence f . i <> 0 by PARTFUN3:def 1; :: thesis: verum

end;

hence not f is multiplicative-trivial ; :: thesis: verum