let b, k be Nat; :: thesis: for f being k -element XFinSequence of NAT holds value ((f ^ <%0%>),b) = value (f,b)
let f be k -element XFinSequence of NAT ; :: thesis: value ((f ^ <%0%>),b) = value (f,b)
value ((f ^ <%0%>),b) = (0 * (b |^ k)) + (value (f,b)) by VFN;
hence value ((f ^ <%0%>),b) = value (f,b) ; :: thesis: verum