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

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