let m be non empty Element of NAT ; :: thesis: for v being Element of REAL m
for x being Element of REAL
for i being Element of NAT holds len (Replace v,i,x) = m
let v be Element of REAL m; :: thesis: for x being Element of REAL
for i being Element of NAT holds len (Replace v,i,x) = m
let x be Element of REAL ; :: thesis: for i being Element of NAT holds len (Replace v,i,x) = m
let i be Element of NAT ; :: thesis: len (Replace v,i,x) = m
len (Replace v,i,x) = len v by FUNCT_7:99;
hence len (Replace v,i,x) = m by FINSEQ_1:def 18; :: thesis: verum