let m be non zero Nat; :: thesis: for v being Element of REAL m
for x being Real
for i being Nat holds len (Replace (v,i,x)) = m
let v be Element of REAL m; :: thesis: for x being Real
for i being Nat holds len (Replace (v,i,x)) = m
let x be Real; :: thesis: for i being Nat holds len (Replace (v,i,x)) = m
let i be 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