let A, B be MP-wff; :: thesis:
set e = elementary_tree 2;
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
A1: not <*1*> is_a_proper_prefix_of <*0*> by TREES_1:52;
A2: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then A3: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def 11;
( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
then A4: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def 9;
then A5: dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def 11;
then reconsider u = <*1*> as Element of dom (A '&' B) by A4, TREES_1:def 9;
<*0*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def 9;
then reconsider o = <*0*> as Element of dom (A '&' B) by A4, A5, A1, TREES_1:def 9;

now :: thesis:

let s be FinSequence of NAT ; :: thesis:
thus ( s in dom A implies o ^ s in dom (A '&' B) ) :: thesis:

proof

assume s in dom A ; :: thesis:
then A6: o ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def 9;
not <*1*> is_a_proper_prefix_of o ^ s by Th2;
hence o ^ s in dom (A '&' B) by A4, A5, A6, TREES_1:def 9; :: thesis:

end;

assume A7: o ^ s in dom (A '&' B) ; :: thesis:

now :: thesis:

per cases ;

suppose s = {} ; :: thesis:

hence s in dom A by TREES_1:22; :: thesis:

end;

suppose A8: s <> {} ; :: thesis:

for w being FinSequence of NAT holds
( not w in dom B or not o ^ s = <*1*> ^ w ) by TREES_1:1, TREES_1:50;
then A9: o ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A5, A7, TREES_1:def 9;
o is_a_proper_prefix_of o ^ s by A8, TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom A & o ^ s = o ^ w ) by A2, A3, A9, TREES_1:def 9;
hence s in dom A by FINSEQ_1:33; :: thesis:

end;

end;

end;

hence s in dom A ; :: thesis:

end;

then A10: dom A = (dom (A '&' B)) | o by TREES_1:def 6;

now :: thesis:

let s be FinSequence of NAT ; :: thesis:
thus ( s in dom B implies u ^ s in dom (A '&' B) ) by A4, A5, TREES_1:def 9; :: thesis:
assume A11: u ^ s in dom (A '&' B) ; :: thesis:

now :: thesis:

per cases ;

suppose s = {} ; :: thesis:

hence s in dom B by TREES_1:22; :: thesis:

end;

suppose s <> {} ; :: thesis:

then <*1*> is_a_proper_prefix_of u ^ s by TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom B & u ^ s = <*1*> ^ w ) by A4, A5, A11, TREES_1:def 9;
hence s in dom B by FINSEQ_1:33; :: thesis:

end;

end;

end;

hence s in dom B ; :: thesis:

end;

then A12: dom B = (dom (A '&' B)) | u by TREES_1:def 6;
o <> Root (dom (A '&' B)) ;
hence card (dom A) < card (dom (A '&' B)) by A10, Th16; :: thesis:
u <> Root (dom (A '&' B)) ;
hence card (dom B) < card (dom (A '&' B)) by A12, Th16; :: thesis: