let D be non empty set ; for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
let p1, p2, p3, q be Element of D; Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
set f = <*p1,p2,p3*>;
A1: 3 -' 1 =
(2 + 1) -' 1
.=
2
by NAT_D:34
;
A2:
len <*p1,p2,p3*> = 3
by FINSEQ_1:45;
then A3:
1 in dom <*p1,p2,p3*>
by FINSEQ_3:25;
A4:
2 in dom <*p1,p2,p3*>
by A2, FINSEQ_3:25;
3 <= len <*p1,p2,p3*>
by FINSEQ_1:45;
then Replace (<*p1,p2,p3*>,3,q) =
((<*p1,p2,p3*> | (3 -' 1)) ^ <*q*>) ^ (<*p1,p2,p3*> /^ 3)
by Def1
.=
((<*p1,p2,p3*> | 2) ^ <*q*>) ^ (<*p1,p2,p3*> /^ (len <*p1,p2,p3*>))
by A1, FINSEQ_1:45
.=
((<*p1,p2,p3*> | 2) ^ <*q*>) ^ {}
by RFINSEQ:27
.=
(<*p1,p2,p3*> | 2) ^ <*q*>
by FINSEQ_1:34
.=
<*(<*p1,p2,p3*> /. 1),(<*p1,p2,p3*> /. 2)*> ^ <*q*>
by A2, FINSEQ_5:81
.=
(<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> /. 2)*>) ^ <*q*>
by A3, PARTFUN1:def 6
.=
(<*(<*p1,p2,p3*> . 1)*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*>
by A4, PARTFUN1:def 6
.=
(<*p1*> ^ <*(<*p1,p2,p3*> . 2)*>) ^ <*q*>
by FINSEQ_1:45
.=
(<*p1*> ^ <*p2*>) ^ <*q*>
by FINSEQ_1:45
;
hence
Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
; verum