let D be non empty set ; :: thesis: for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>
let p1, p2, p3, q be Element of D; :: thesis: Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>
set f = <*p1,p2,p3*>;
len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then Replace (<*p1,p2,p3*>,1,q) = ((<*p1,p2,p3*> | (1 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 1) by Def1
.= ((<*p1,p2,p3*> | 0) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 1) by XREAL_1:232
.= <*q*> ^ (<*p1,p2,p3*> /^ 1) by FINSEQ_1:34
.= <*q*> ^ <*p2,p3*> by FINSEQ_6:47
.= (<*q*> ^ <*p2*>) ^ <*p3*> by FINSEQ_1:32 ;
hence Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*> ; :: thesis: verum