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 b1 being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b1 = Replace (f,i,p) iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace (f,i,p) iff b1 = f ) ) ) by A1; :: thesis: verum