let n be non empty Element of NAT ; :: thesis: 0.REAL n <> 1.REAL n
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:3;
then A1: ( (n |-> 0) . 1 = 0 & (n |-> 1) . 1 = 1 ) by FINSEQ_2:71;
1.REAL n = 1* n by JORDAN2C:def 8
.= n |-> 1 by JORDAN2C:def 7 ;
hence 0.REAL n <> 1.REAL n by A1, EUCLID:def 4; :: thesis: verum