set p = <*0*>;
for u being object st u in {0} holds
u in INT by INT_1:def 1;
then {0} c= INT by TARSKI:def 3;
then rng <*0*> c= INT by FINSEQ_1:39;
then reconsider f = <*0*> as FinSequence of INT by FINSEQ_1:def 4;
take f ; :: thesis: f is multiplicative-trivial
take 1 ; :: according to INT_6:def 1 :: thesis: ( 1 in dom f & f . 1 = 0 )
len f = 1 by FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:def 3;
hence 1 in dom f ; :: thesis: f . 1 = 0
thus f . 1 = 0 by FINSEQ_1:40; :: thesis: verum