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