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 9; :: thesis: ( ( for i being natural number holds
( not i in dom f or not f . i = 0 ) ) implies not f is multiplicative-trivial )
assume A1: 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 9 :: thesis: ( not n in findom f or not f . n is empty )
assume n in dom f ; :: thesis: not f . n is empty
hence not f . n is empty by A1; :: thesis: verum