n is Element of NAT by ORDINAL1:def 12;
A: n = len (n |-> (0. R)) by FINSEQ_2:132
.= len (Replace ((n |-> (0. R)),i,(1. R))) by FINSEQ_7:5 ;
reconsider u = Replace ((n |-> (0. R)),i,(1. R)) as Element of the carrier of R * by FINSEQ_1:def 11;
u in { s where s is Element of the carrier of R * : len s = n } by A;
hence Replace ((n |-> (0. R)),i,(1. R)) is Element of n -tuples_on the carrier of R by FINSEQ_2:def 4; :: thesis: verum