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