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:62;
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:234
.= <*q*> ^ (<*p1,p2,p3*> /^ 1) by FINSEQ_1:47
.= <*q*> ^ <*p2,p3*> by FINSEQ_6:51
.= (<*q*> ^ <*p2*>) ^ <*p3*> by FINSEQ_1:45 ;
hence Replace <*p1,p2,p3*>,1,q = <*q,p2,p3*> ; :: thesis: verum