set p = <*0*>;

now

let u be set ; :: thesis: ( u in {0} implies u in INT )
assume u in {0} ; :: thesis: u in INT
then reconsider u9 = u as Element of NAT by TARSKI:def 1;
u9 is integer number ;
hence u in INT by INT_1:def 1; :: thesis: verum

end;

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