let a, b be set ; :: thesis: Replace (<%a%>,0,b) = <%b%>
A1: len (Replace (<%a%>,0,b)) = len <%a%> by FUNCT_7:30
.= 1 by AFINSQ_1:34 ;
0 in Segm 1 by NAT_1:44;
then 0 in dom <%a%> by AFINSQ_1:33;
then (Replace (<%a%>,0,b)) . 0 = b by FUNCT_7:31;
hence Replace (<%a%>,0,b) = <%b%> by A1, AFINSQ_1:34; :: thesis: verum