let T be Tree; :: thesis: for p being Tree-yielding FinSequence holds tree (p ^ <*T*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T
let p be Tree-yielding FinSequence; :: thesis: tree (p ^ <*T*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T
set W1 = elementary_tree ((len p) + 1);
set W2 = (tree p) \/ (elementary_tree ((len p) + 1));
set W = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T;
len <*T*> = 1 by FINSEQ_1:57;
then A1: len (p ^ <*T*>) = (len p) + 1 by FINSEQ_1:35;
len p < (len p) + 1 by NAT_1:13;
then <*(len p)*> in elementary_tree ((len p) + 1) by TREES_1:55;
then A2: <*(len p)*> in (tree p) \/ (elementary_tree ((len p) + 1)) by XBOOLE_0:def 3;
let q be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not q in tree (p ^ <*T*>) or q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T ) & ( not q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T or q in tree (p ^ <*T*>) ) )
thus ( q in tree (p ^ <*T*>) implies q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T ) :: thesis: ( not q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T or q in tree (p ^ <*T*>) )

proof

assume q in tree (p ^ <*T*>) ; :: thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T
then A3: ( q = {} or ex n being Element of NAT ex r being FinSequence st
( n < len (p ^ <*T*>) & r in (p ^ <*T*>) . (n + 1) & q = <*n*> ^ r ) ) by Def15;

now

given n being Element of NAT , r being FinSequence such that A4: n < len (p ^ <*T*>) and
A5: r in (p ^ <*T*>) . (n + 1) and
A6: q = <*n*> ^ r ; :: thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T
reconsider r = r as FinSequence of NAT by A6, FINSEQ_1:50;
A7: n <= len p by A1, A4, NAT_1:13;

A8: now

assume A9: n < len p ; :: thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T
then n + 1 in dom p by Lm4;
then (p ^ <*T*>) . (n + 1) = p . (n + 1) by FINSEQ_1:def 7;
then q in tree p by A5, A6, A9, Def15;
then A10: q in (tree p) \/ (elementary_tree ((len p) + 1)) by XBOOLE_0:def 3;
not <*(len p)*> is_a_prefix_of <*n*> ^ r by A9, TREES_1:87;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ r by XBOOLE_0:def 8;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T by A2, A6, A10, TREES_1:def 12; :: thesis: verum

end;

now

assume A11: n = len p ; :: thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T
then A12: (p ^ <*T*>) . (n + 1) = T by FINSEQ_1:59;
r = r ;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T by A2, A5, A6, A11, A12, TREES_1:def 12; :: thesis: verum

end;

hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T by A7, A8, XXREAL_0:1; :: thesis: verum

end;

hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T by A3, TREES_1:47; :: thesis: verum

end;

assume A13: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,T ; :: thesis: q in tree (p ^ <*T*>)
assume A14: not q in tree (p ^ <*T*>) ; :: thesis: contradiction

A15: now

given r being FinSequence of NAT such that A16: r in T and
A17: q = <*(len p)*> ^ r ; :: thesis: contradiction
A18: len p < (len p) + 1 by NAT_1:13;
(p ^ <*T*>) . ((len p) + 1) = T by FINSEQ_1:59;
hence contradiction by A1, A14, A16, A17, A18, Def15; :: thesis: verum

end;

now

assume q in (tree p) \/ (elementary_tree ((len p) + 1)) ; :: thesis: contradiction
then A19: ( q in tree p or q in elementary_tree ((len p) + 1) ) by XBOOLE_0:def 3;

A20: now

assume q in tree p ; :: thesis: contradiction
then ( ( q = {} & {} in tree (p ^ <*T*>) ) or ex n being Element of NAT ex r being FinSequence st
( n < len p & r in p . (n + 1) & q = <*n*> ^ r ) ) by Def15;
then consider n being Element of NAT , r being FinSequence such that
A21: n < len p and
A22: r in p . (n + 1) and
A23: q = <*n*> ^ r by A14;
n + 1 in dom p by A21, Lm4;
then A24: p . (n + 1) = (p ^ <*T*>) . (n + 1) by FINSEQ_1:def 7;
n < len (p ^ <*T*>) by A1, A21, NAT_1:13;
hence contradiction by A14, A22, A23, A24, Def15; :: thesis: verum

end;

now

assume A25: not q in tree p ; :: thesis: contradiction
then ( q = {} or ex n being Element of NAT st
( n < (len p) + 1 & q = <*n*> ) ) by A19, TREES_1:57;
then consider n being Element of NAT such that
A26: n < (len p) + 1 and
A27: q = <*n*> by A14, TREES_1:47;

A28: now

assume n < len p ; :: thesis: {} in p . (n + 1)
then A29: p . (n + 1) in rng p by Lm4;
rng p is constituted-Trees by Def9;
then p . (n + 1) is Tree by A29, Def3;
hence {} in p . (n + 1) by TREES_1:47; :: thesis: verum

end;

A30: q = <*n*> ^ {} by A27, FINSEQ_1:47;
then A31: n >= len p by A25, A28, Def15;
n <= len p by A26, NAT_1:13;
then A32: len p = n by A31, XXREAL_0:1;
A33: n < n + 1 by NAT_1:13;
A34: (p ^ <*T*>) . ((len p) + 1) = T by FINSEQ_1:59;
{} in T by TREES_1:47;
hence contradiction by A1, A14, A30, A32, A33, A34, Def15; :: thesis: verum

end;

hence contradiction by A20; :: thesis: verum

end;

hence contradiction by A2, A13, A15, TREES_1:def 12; :: thesis: verum