let D be non empty set ; :: thesis: for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*>
let p, q be Element of D; :: thesis: Replace (<*p*>,1,q) = <*q*>
A1: 1 - 1 = 0 ;
set g = <*> D;
reconsider P = <*p*> ^ (<*> D) as FinSequence of D ;
A2: (<*p*> ^ (<*> D)) /^ 1 = <*> D by FINSEQ_6:45;
1 <= len <*p*> by FINSEQ_1:39;
hence Replace (<*p*>,1,q) = ((<*p*> | (1 -' 1)) ^ <*q*>) ^ (<*p*> /^ 1) by Def1
.= ((<*p*> | 0) ^ <*q*>) ^ (<*p*> /^ 1) by A1, XREAL_0:def 2
.= <*q*> ^ (<*p*> /^ 1) by FINSEQ_1:34
.= <*q*> ^ (P /^ 1) by FINSEQ_1:34
.= <*q*> by A2, FINSEQ_1:34 ;
:: thesis: verum