let n, m be Nat; :: thesis: for s being FinSequence st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s
let s be FinSequence; :: thesis: ( n <> m implies not <*n*> is_a_prefix_of <*m*> ^ s )
assume A1: n <> m ; :: thesis: not <*n*> is_a_prefix_of <*m*> ^ s
assume <*n*> is_a_prefix_of <*m*> ^ s ; :: thesis: contradiction
then A2: ex a being FinSequence st <*m*> ^ s = <*n*> ^ a by Th1;
m = (<*m*> ^ s) . 1 by FINSEQ_1:41
.= n by A2, FINSEQ_1:41 ;
hence contradiction by A1; :: thesis: verum