A1: ( ( not 1 <= i or not i <= len f ) implies f +* (i,p) = f )

proof

assume ( not 1 <= i or not i <= len f ) ; :: thesis: f +* (i,p) = f
then not i in dom f by FINSEQ_3:25;
hence f +* (i,p) = f by FUNCT_7:def 3; :: thesis: verum

end;

( 1 <= i & i <= len f implies f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) )

proof

assume ( 1 <= i & i <= len f ) ; :: thesis: f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)
then i in dom f by FINSEQ_3:25;
hence f +* (i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) by FUNCT_7:98; :: thesis: verum

end;

hence for b₁ being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b₁ = Replace (f,i,p) iff b₁ = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b₁ = Replace (f,i,p) iff b₁ = f ) ) ) by A1; :: thesis: verum