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

hence
not f is multiplicative-trivial
; :: thesis: verumf . 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;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