let p be XFinSequence; :: thesis: for i being Element of NAT
for x being set holds
( len (Replace p,i,x) = len p & ( i < len p implies (Replace p,i,x) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace p,i,x) . j = p . j ) )
let i be Element of NAT ; :: thesis: for x being set holds
( len (Replace p,i,x) = len p & ( i < len p implies (Replace p,i,x) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace p,i,x) . j = p . j ) )
let x be set ; :: thesis: ( len (Replace p,i,x) = len p & ( i < len p implies (Replace p,i,x) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace p,i,x) . j = p . j ) )
set f = Replace p,i,x;
thus len (Replace p,i,x) = len p by FUNCT_7:32; :: thesis: ( ( i < len p implies (Replace p,i,x) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace p,i,x) . j = p . j ) )
( i < len p implies not dom p c= i ) by NAT_1:40;
hence ( i < len p implies (Replace p,i,x) . i = x ) by FUNCT_7:33, ORDINAL1:26; :: thesis: for j being Element of NAT st j <> i holds
(Replace p,i,x) . j = p . j
thus for j being Element of NAT st j <> i holds
(Replace p,i,x) . j = p . j by FUNCT_7:34; :: thesis: verum