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