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