let n be 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:1;
assume A2: 1* n = 0* n ; :: thesis: contradiction
( 1* n = n |-> 1 & (n |-> 0) . 1 = 0 ) by A1, FUNCOP_1:7;
hence contradiction by A2, A1, FUNCOP_1:7; :: thesis: verum