let n be Element of NAT ; :: thesis: ( n >= 1 implies 1* n <> 0* n )
assume n >= 1 ; :: thesis: 1* n <> 0* n
then A1: 1 in Seg n by FINSEQ_1:3;
assume A2: 1* n = 0* n ; :: thesis: contradiction
( 1* n = n |-> 1 & (n |-> 0 ) . 1 = 0 ) by A1, FUNCOP_1:13, JORDAN2C:def 7;
hence contradiction by A2, A1, FUNCOP_1:13; :: thesis: verum