theorem :: NUMBER17:59

for a, b, c being set holds Replace (<%a,b%>,1,c) = <%a,c%>