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