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