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:97;
hence len (Replace (v,i,x)) = m by CARD_1:def 7; :: thesis: verum