let p, q be Tree-yielding FinSequence; :: thesis: for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) holds
for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement <*k*>,t
let k be Element of NAT ; :: thesis: ( len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) implies for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement <*k*>,t )
assume that
A1:
len p = len q
and
A2:
k + 1 in dom p
and
A3:
for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i
; :: thesis: for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement <*k*>,t
set o = <*k*>;
k + 1 <= len p
by A2, FINSEQ_3:27;
then A4:
k < len p
by NAT_1:13;
let t be Tree; :: thesis: ( q . (k + 1) = t implies tree q = (tree p) with-replacement <*k*>,t )
assume A5:
q . (k + 1) = t
; :: thesis: tree q = (tree p) with-replacement <*k*>,t
p . (k + 1) is Tree
by A2, TREES_3:24;
then A6:
{} in p . (k + 1)
by TREES_1:47;
<*k*> = <*k*> ^ {}
by FINSEQ_1:47;
then A7:
<*k*> in tree p
by A4, A6, TREES_3:def 15;
hence
tree q = (tree p) with-replacement <*k*>,t
by A7, TREES_1:def 12; :: thesis: verum