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:40;
then A1: len (p ^ <*T*>) = (len p) + 1 by FINSEQ_1:22;
len p < (len p) + 1 by NAT_1:13;
then <*(len p)*> in elementary_tree ((len p) + 1) by TREES_1:28;
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 Nat ex r being FinSequence st
( n < len (p ^ <*T*>) & r in (p ^ <*T*>) . (n + 1) & q = <*n*> ^ r ) ) by Def15;

now :: thesis: ( ex n being Nat ex r being FinSequence st
( n < len (p ^ <*T*>) & r in (p ^ <*T*>) . (n + 1) & q = <*n*> ^ r ) implies q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) )

given n being 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:36;
A7: n <= len p by A1, A4, NAT_1:13;

A8: now :: thesis: ( n < len p implies q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) )

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 Lm3;
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:50;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ r ;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) by A2, A6, A10, TREES_1:def 9; :: thesis: verum

end;

now :: thesis: ( n = len p implies q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) )

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:42;
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 9; :: 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:22; :: 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 :: thesis: for r being FinSequence of NAT holds
( not r in T or not q = <*(len p)*> ^ r )

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:42;
hence contradiction by A1, A14, A16, A17, A18, Def15; :: thesis: verum

end;

now :: thesis: not q in (tree p) \/ (elementary_tree ((len p) + 1))

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 :: thesis: not q in tree p

assume q in tree p ; :: thesis: contradiction
then ( ( q = {} & {} in tree (p ^ <*T*>) ) or ex n being Nat ex r being FinSequence st
( n < len p & r in p . (n + 1) & q = <*n*> ^ r ) ) by Def15;
then consider n being 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, Lm3;
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 :: thesis: q in tree p

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

A28: now :: thesis: ( n < len p implies {} in p . (n + 1) )

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

end;

A30: q = <*n*> ^ {} by A27, FINSEQ_1:34;
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:42;
{} in T by TREES_1:22;
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 9; :: thesis: verum