let D be non empty set ; :: thesis: for p1, p2, p3, q being Element of D holds Replace <*p1,p2,p3*>,3,q = <*p1,p2,q*>
let p1, p2, p3, q be Element of D; :: thesis: Replace <*p1,p2,p3*>,3,q = <*p1,p2,q*>
set f = <*p1,p2,p3*>;
A1: 3 -' 1 = (2 + 1) -' 1
.= 2 by NAT_D:34 ;
A2: len <*p1,p2,p3*> = 3 by FINSEQ_1:62;
then A3: 1 in dom <*p1,p2,p3*> by FINSEQ_3:27;
A4: 2 in dom <*p1,p2,p3*> by A2, FINSEQ_3:27;
3 <= len <*p1,p2,p3*> by FINSEQ_1:62;
then Replace <*p1,p2,p3*>,3,q = ((<*p1,p2,p3*> | (3 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 3) by Def1
.= ((<*p1,p2,p3*> | 2) ^ <*q*>) ^ (<*p1,p2,p3*> /^ (len <*p1,p2,p3*>)) by A1, FINSEQ_1:62
.= ((<*p1,p2,p3*> | 2) ^ <*q*>) ^ {} by RFINSEQ:40
.= (<*p1,p2,p3*> | 2) ^ <*q*> by FINSEQ_1:47
.= <*(<*p1,p2,p3*> /. 1),(<*p1,p2,p3*> /. 2)*> ^ <*q*> by A2, FINSEQ_5:84
.= (<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> /. 2)*>) ^ <*q*> by A3, PARTFUN1:def 8
.= (<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*> by A4, PARTFUN1:def 8
.= (<*p1*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*> by FINSEQ_1:62
.= (<*p1*> ^ <*p2*>) ^ <*q*> by FINSEQ_1:62 ;
hence Replace <*p1,p2,p3*>,3,q = <*p1,p2,q*> ; :: thesis: verum