let p, q be Tree-yielding FinSequence; :: thesis: for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
let T1, T2 be Tree; :: thesis: tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
set w1 = (p ^ <*T1*>) ^ q;
set W1 = tree ((p ^ <*T1*>) ^ q);
set w2 = (p ^ <*T2*>) ^ q;
set W2 = tree ((p ^ <*T2*>) ^ q);
set W = (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1;
( len <*T1*> = 1 & len <*T2*> = 1 ) by FINSEQ_1:57;
then A1: ( len (p ^ <*T1*>) = (len p) + 1 & len ((p ^ <*T1*>) ^ q) = (len (p ^ <*T1*>)) + (len q) & len (p ^ <*T2*>) = (len p) + 1 & len ((p ^ <*T2*>) ^ q) = (len (p ^ <*T2*>)) + (len q) ) by FINSEQ_1:35;
( len p < (len p) + 1 & (len p) + 1 <= ((len p) + 1) + (len q) ) by NAT_1:11, NAT_1:13;
then A2: len p < ((len p) + 1) + (len q) by XXREAL_0:2;
then ( ((p ^ <*T2*>) ^ q) . ((len p) + 1) in rng ((p ^ <*T2*>) ^ q) & rng ((p ^ <*T2*>) ^ q) is constituted-Trees ) by A1, Def9, Lm4;
then ((p ^ <*T2*>) ^ q) . ((len p) + 1) is Tree by Def3;
then ( {} in ((p ^ <*T2*>) ^ q) . ((len p) + 1) & <*(len p)*> ^ {} = <*(len p)*> ) by FINSEQ_1:47, TREES_1:47;
then A3: <*(len p)*> in tree ((p ^ <*T2*>) ^ q) by A1, A2, Def15;
let r be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not r in tree ((p ^ <*T1*>) ^ q) or r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 ) & ( not r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 or r in tree ((p ^ <*T1*>) ^ q) ) )
thus ( r in tree ((p ^ <*T1*>) ^ q) implies r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 ) :: thesis: ( not r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 or r in tree ((p ^ <*T1*>) ^ q) )

proof

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

now

given n being Element of NAT , s being FinSequence such that A5: ( n < len ((p ^ <*T1*>) ^ q) & s in ((p ^ <*T1*>) ^ q) . (n + 1) & r = <*n*> ^ s ) ; :: thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
reconsider s = s as FinSequence of NAT by A5, FINSEQ_1:50;
A6: ( n <= len p or n >= (len p) + 1 ) by NAT_1:13;

A7: now

assume A8: n < len p ; :: thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
then ( n + 1 in dom p & dom p c= dom (p ^ <*T2*>) & dom p c= dom (p ^ <*T1*>) ) by Lm4, FINSEQ_1:39;
then ( (p ^ <*T2*>) . (n + 1) = p . (n + 1) & (p ^ <*T1*>) . (n + 1) = p . (n + 1) & n + 1 in dom (p ^ <*T1*>) & n + 1 in dom (p ^ <*T2*>) ) by FINSEQ_1:def 7;
then ( ((p ^ <*T2*>) ^ q) . (n + 1) = p . (n + 1) & ((p ^ <*T1*>) ^ q) . (n + 1) = p . (n + 1) ) by FINSEQ_1:def 7;
then A9: r in tree ((p ^ <*T2*>) ^ q) by A1, A5, Def15;
not <*(len p)*> is_a_prefix_of <*n*> ^ s by A8, TREES_1:87;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ s by XBOOLE_0:def 8;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 by A3, A5, A9, TREES_1:def 12; :: thesis: verum

end;

A10: now

assume A11: n = len p ; :: thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
then A12: (p ^ <*T1*>) . (n + 1) = T1 by FINSEQ_1:59;
n < (len p) + 1 by A11, NAT_1:13;
then n + 1 in dom (p ^ <*T1*>) by A1, Lm4;
then ( ((p ^ <*T1*>) ^ q) . (n + 1) = T1 & s = s ) by A12, FINSEQ_1:def 7;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 by A3, A5, A11, TREES_1:def 12; :: thesis: verum

end;

now

assume A13: ( n >= (len p) + 1 & n < ((len p) + 1) + (len q) ) ; :: thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1
then ( n + 1 >= ((len p) + 1) + 1 & n + 1 <= ((len p) + 1) + (len q) ) by NAT_1:13, XREAL_1:9;
then ( ((p ^ <*T1*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) & ((p ^ <*T2*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) ) by A1, FINSEQ_1:36;
then A14: r in tree ((p ^ <*T2*>) ^ q) by A1, A5, Def15;
len p <> n by A13, NAT_1:13;
then not <*(len p)*> is_a_prefix_of <*n*> ^ s by TREES_1:87;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ s by XBOOLE_0:def 8;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 by A3, A5, A14, TREES_1:def 12; :: thesis: verum

end;

hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 by A1, A5, A6, A7, A10, XXREAL_0:1; :: thesis: verum

end;

hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 by A4, TREES_1:47; :: thesis: verum

end;

assume r in (tree ((p ^ <*T2*>) ^ q)) with-replacement <*(len p)*>,T1 ; :: thesis: r in tree ((p ^ <*T1*>) ^ q)
then A15: ( ( r in tree ((p ^ <*T2*>) ^ q) & not <*(len p)*> is_a_proper_prefix_of r ) or ex s being FinSequence of NAT st
( s in T1 & r = <*(len p)*> ^ s ) ) by A3, TREES_1:def 12;
assume A16: not r in tree ((p ^ <*T1*>) ^ q) ; :: thesis: contradiction
then A17: ( r <> {} & ( for n being Element of NAT
for q being FinSequence st n < len ((p ^ <*T1*>) ^ q) & q in ((p ^ <*T1*>) ^ q) . (n + 1) holds
r <> <*n*> ^ q ) ) by Def15;
A18: (p ^ <*T1*>) . ((len p) + 1) = T1 by FINSEQ_1:59;
( len p < (len p) + 1 & (len p) + 1 <= ((len p) + 1) + (len q) ) by NAT_1:11, NAT_1:13;
then A19: ( len p < len ((p ^ <*T2*>) ^ q) & (len p) + 1 in dom (p ^ <*T1*>) ) by A1, Lm4, XXREAL_0:2;
then A20: ((p ^ <*T1*>) ^ q) . ((len p) + 1) = T1 by A18, FINSEQ_1:def 7;
then consider n being Element of NAT , s being FinSequence such that
A21: ( n < len ((p ^ <*T2*>) ^ q) & s in ((p ^ <*T2*>) ^ q) . (n + 1) & r = <*n*> ^ s ) by A1, A15, A17, A19, Def15;
reconsider s = s as FinSequence of NAT by A21, FINSEQ_1:50;
( ( n = len p implies s = {} ) & {} in T1 ) by A1, A15, A16, A20, A21, Def15, TREES_1:33, TREES_1:47;
then ( n <> len p & ( n <= len p or n >= len p ) ) by A1, A16, A20, A21, Def15;
then ( n < len p or ( n > len p & 1 <= 1 ) ) by XXREAL_0:1;
then ( ( 1 <= 1 + n & 1 + n = n + 1 & n + 1 <= len p & (p ^ <*T1*>) ^ q = p ^ (<*T1*> ^ q) & (p ^ <*T2*>) ^ q = p ^ (<*T2*> ^ q) ) or ( (len p) + 1 < n + 1 & n + 1 <= len ((p ^ <*T1*>) ^ q) ) ) by A1, A21, FINSEQ_1:45, NAT_1:11, NAT_1:13, XREAL_1:8;
then ( ( ((p ^ <*T1*>) ^ q) . (n + 1) = p . (n + 1) & ((p ^ <*T2*>) ^ q) . (n + 1) = p . (n + 1) ) or ( ((p ^ <*T1*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) & ((p ^ <*T2*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) ) ) by A1, Lm1, FINSEQ_1:37;
hence contradiction by A1, A16, A21, Def15; :: thesis: verum