let n be non zero Nat; :: thesis: 0.REAL n <> 1.REAL n
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then A1: ( (n |-> 0) . 1 = 0 & (n |-> 1) . 1 = 1 ) by FINSEQ_2:57;
1.REAL n = 1* n by EUCLID:def 12
.= n |-> 1 by EUCLID:def 11 ;
hence 0.REAL n <> 1.REAL n by A1, EUCLID:def 4; :: thesis: verum