let A, B, C be MP-wff; :: thesis: (#) A <> B '&' C
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:55, TREES_1:89;
A2: ( <*0 *> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 ) by FUNCOP_1:19, TREES_1:55;
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 12;
then A3: <*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,B) by A2, A1, TREES_1:def 12;
then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,B)) with-replacement <*1*>,(dom C) by TREES_2:def 12;
then A4: <*1*> in dom (B '&' C) by A3, TREES_1:def 12;
assume A5: not (#) A <> B '&' C ; :: thesis: contradiction
A6: dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 by FUNCOP_1:19;

A7: now

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

end;

<*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
then A8: <*0 *> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:19;
then dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) with-replacement <*0 *>,(dom A) by TREES_2:def 12;
then ex s being FinSequence of NAT st
( s in dom A & <*1*> = <*0 *> ^ s ) by A8, A4, A7, A5, TREES_1:def 12;
then <*0 *> is_a_prefix_of <*1*> by TREES_1:8;
hence contradiction by TREES_1:16; :: thesis: verum