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:30; :: 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 Segm (len p) c= Segm i ) by NAT_1:39;
hence ( i < len p implies (Replace (p,i,x)) . i = x ) by FUNCT_7:31, ORDINAL1:16; :: 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:32; :: thesis: verum