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:44;
1 + 1 = len <*p1,p2*> by FINSEQ_1:44;
then A3: <*p1,p2*> /^ 1 = <*(<*p1,p2*> . 2)*> by FINSEQ_5:30;
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:232
.= ({} ^ <*q*>) ^ <*p2*> by A3, FINSEQ_1:44
.= <*q*> ^ <*p2*> by FINSEQ_1:34 ;
hence Replace (<*p1,p2*>,1,q) = <*q,p2*> ; :: thesis: verum