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:56;
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:57;
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:57; :: thesis: verum