thus ( not f is multiplicative-trivial implies for i being natural number holds
( not i in dom f or not f . i = 0 ) ) by FUNCT_1:def 15; :: thesis: ( ( for i being natural number holds
( not i in dom f or not f . i = 0 ) ) implies not f is multiplicative-trivial )
assume Z1: for i being natural number holds
( not i in dom f or not f . i = 0 ) ; :: thesis: not f is multiplicative-trivial
let n be set ; :: according to FUNCT_1:def 15 :: thesis: ( not n in findom f or not f . n is empty )
assume Z2: n in dom f ; :: thesis: not f . n is empty
thus not f . n is empty by Z1, Z2; :: thesis: verum