let D be non empty set ; :: thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>
let p1, p2, p3, q be Element of D; :: thesis: Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>
set f = <*p1,p2,p3*>;
A1: 2 -' 1 = (1 + 1) -' 1
.= 1 by NAT_D:34 ;
A2: len <*p1,p2,p3*> = 2 + 1 by FINSEQ_1:45;
A3: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then A4: 3 in dom <*p1,p2,p3*> by FINSEQ_3:25;
A5: 1 in dom <*p1,p2,p3*> by A3, FINSEQ_3:25;
Replace (<*p1,p2,p3*>,2,q) = ((<*p1,p2,p3*> | (2 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 2) by A3, Def1
.= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*(<*p1,p2,p3*> /. 3)*> by A1, A2, FINSEQ_5:30
.= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*(<*p1,p2,p3*> . 3)*> by A4, PARTFUN1:def 6
.= ((<*p1,p2,p3*> | 1) ^ <*q*>) ^ <*p3*> by FINSEQ_1:45
.= (<*(<*p1,p2,p3*> /. 1)*> ^ <*q*>) ^ <*p3*> by FINSEQ_5:20
.= (<*(<*p1,p2,p3*> . 1)*> ^ <*q*>) ^ <*p3*> by A5, PARTFUN1:def 6
.= (<*p1*> ^ <*q*>) ^ <*p3*> by FINSEQ_1:45 ;
hence Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*> ; :: thesis: verum