let A, B, C be MP-wff; :: thesis:
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
set F = (elementary_tree 1) --> [1,1];
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B);
A1: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, 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 dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom B)) by TREES_2:def 11;
then A3: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) by A2, A1, TREES_1:def 9;
then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))) with-replacement (<*1*>,(dom C)) by TREES_2:def 11;
then A4: <*1*> in dom (B '&' C) by A3, TREES_1:def 9;
assume A5: not (#) A <> B '&' C ; :: thesis:

A6: now :: thesis:

assume <*1*> in dom ((elementary_tree 1) --> [1,1]) ; :: thesis:
then ( <*1*> = {} or <*1*> = <*0*> ) by TARSKI:def 2, TREES_1:51;
hence contradiction by TREES_1:3; :: thesis:

end;

<*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
then A7: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13;
then dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by TREES_2:def 11;
then ex s being FinSequence of NAT st
( s in dom A & <*1*> = <*0*> ^ s ) by A7, A4, A6, A5, TREES_1:def 9;
then <*0*> is_a_prefix_of <*1*> by TREES_1:1;
hence contradiction by TREES_1:3; :: thesis: