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