set p = <*1*>;

now

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

end;

then {1} c= INT by TARSKI:def 3;
then rng <*1*> c= INT by FINSEQ_1:56;
then reconsider f = <*1*> as FinSequence of INT by FINSEQ_1:def 4;
take f ; :: thesis: not f is multiplicative-trivial

H: now

let i be Element of NAT ; :: thesis: ( i in dom f implies i = 1 )
assume i in dom f ; :: thesis: i = 1
then i in Seg 1 by FINSEQ_1:55;
hence i = 1 by FINSEQ_1:4, TARSKI:def 1; :: thesis: verum

end;

now

assume ex i being natural number st
( i in dom f & f . i = 0 ) ; :: thesis: contradiction
then consider i being natural number such that
A: ( i in dom f & f . i = 0 ) ;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
i = 1 by A, H;
hence contradiction by A, FINSEQ_1:57; :: thesis: verum

end;

hence not f is multiplicative-trivial by DefMTriv; :: thesis: verum