A1: ( 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:27;
hence f +* i,p = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) by FUNCT_7:100; :: thesis: verum

end;

( ( 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:27;
hence f +* i,p = f by FUNCT_7:def 3; :: thesis: verum

end;

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