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