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:49;
( 1 <= 1 & 1 <= len <*p*> ) by FINSEQ_1:56;
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:47
.= <*q*> ^ (P /^ 1) by FINSEQ_1:47
.= <*q*> by A2, FINSEQ_1:47 ;
:: thesis: verum