let A, A1, B, B1 be MP-wff; :: thesis:
set e = elementary_tree 2;
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
set y1 = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1);
assume A1: A '&' B = A1 '&' B1 ; :: thesis:
A2: <*1*> in elementary_tree 2 by TREES_1:28;
A3: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28;
then A4: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A1)) by TREES_2:def 11;
not <*1*> is_a_proper_prefix_of <*0*> by TREES_1:52;
then A5: <*0*> in (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(dom B)) by A2, A3, TREES_1:def 9;
A6: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52;
then A7: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) by A2, A3, A4, TREES_1:def 9;
A8: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A3, TREES_2:def 11;
then A9: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, A6, TREES_1:def 9;
then A10: dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def 11;
A11: dom (A1 '&' B1) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1))) with-replacement (<*1*>,(dom B1)) by A7, TREES_2:def 11;

now :: thesis:

let s be FinSequence of NAT ; :: thesis:
thus ( s in dom B implies s in dom B1 ) :: thesis:

proof

assume s in dom B ; :: thesis:
then A12: <*1*> ^ s in dom (A1 '&' B1) by A1, A9, A10, TREES_1:def 9;

now :: thesis:

per cases ;

suppose s = {} ; :: thesis:

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

end;

suppose s <> {} ; :: thesis:

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

end;

end;

end;

hence s in dom B1 ; :: thesis:

end;

assume s in dom B1 ; :: thesis:
then A13: <*1*> ^ s in dom (A '&' B) by A1, A7, A11, TREES_1:def 9;

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 <*1*> ^ s by TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom B & <*1*> ^ s = <*1*> ^ w ) by A9, A10, A13, 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 A14: dom B = dom B1 by TREES_2:def 1;
A15: for s being FinSequence of NAT st s in dom B holds
B . s = B1 . s

proof

let s be FinSequence of NAT ; :: thesis:
assume s in dom B ; :: thesis:
then A16: <*1*> ^ s in dom (A1 '&' B1) by A1, A9, A10, TREES_1:def 9;
A17: <*1*> is_a_prefix_of <*1*> ^ s by TREES_1:1;
then consider w being FinSequence of NAT such that
w in dom B1 and
A18: <*1*> ^ s = <*1*> ^ w and
A19: (A1 '&' B1) . (<*1*> ^ s) = B1 . w by A7, A11, A16, TREES_2:def 11;
A20: ex u being FinSequence of NAT st
( u in dom B & <*1*> ^ s = <*1*> ^ u & (A '&' B) . (<*1*> ^ s) = B . u ) by A1, A9, A10, A16, A17, TREES_2:def 11;
s = w by A18, FINSEQ_1:33;
hence B . s = B1 . s by A1, A19, A20, FINSEQ_1:33; :: thesis:

end;

then A21: B = B1 by A14, TREES_2:31;
A22: not <*0*>,<*1*> are_c=-comparable by TREES_1:5;
then A23: dom (A '&' B) = ((dom ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(dom B))) with-replacement (<*0*>,(dom A)) by A2, A3, A8, A10, TREES_2:8;
A24: dom (A1 '&' B1) = ((dom ((elementary_tree 2) --> [2,0])) with-replacement (<*1*>,(dom B))) with-replacement (<*0*>,(dom A1)) by A22, A2, A3, A4, A11, A14, TREES_2:8;
then A25: dom A = dom A1 by A1, A5, A23, Th6;
for s being FinSequence of NAT st s in dom A holds
A . s = A1 . s

proof

let s be FinSequence of NAT ; :: thesis:
assume A26: s in dom A ; :: thesis:
then A27: <*0*> ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A3, A8, TREES_1:def 9;
A28: <*0*> is_a_prefix_of <*0*> ^ s by TREES_1:1;
then A29: ex w being FinSequence of NAT st
( w in dom A & <*0*> ^ s = <*0*> ^ w & (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ s) = A . w ) by A3, A8, A27, TREES_2:def 11;
<*0*> ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) by A3, A4, A25, A26, TREES_1:def 9;
then A30: ex u being FinSequence of NAT st
( u in dom A1 & <*0*> ^ s = <*0*> ^ u & (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) . (<*0*> ^ s) = A1 . u ) by A3, A4, A28, TREES_2:def 11;
not <*1*> is_a_proper_prefix_of <*0*> ^ s by Th2;
then A31: <*0*> ^ s in dom (A '&' B) by A9, A10, A27, TREES_1:def 9;
for w being FinSequence of NAT holds
( not w in dom B or not <*0*> ^ s = <*1*> ^ w or not (A '&' B) . (<*0*> ^ s) = B . w ) by TREES_1:1, TREES_1:50;
then (A '&' B) . (<*0*> ^ s) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ s) by A9, A10, A31, TREES_2:def 11;
then A32: A . s = (A1 '&' B) . (<*0*> ^ s) by A1, A21, A29, FINSEQ_1:33;
for w being FinSequence of NAT holds
( not w in dom B1 or not <*0*> ^ s = <*1*> ^ w or not (A1 '&' B1) . (<*0*> ^ s) = B1 . w ) by TREES_1:1, TREES_1:50;
then (A1 '&' B1) . (<*0*> ^ s) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) . (<*0*> ^ s) by A1, A7, A11, A31, TREES_2:def 11;
hence A . s = A1 . s by A21, A32, A30, FINSEQ_1:33; :: thesis:

end;

hence ( A = A1 & B = B1 ) by A1, A5, A14, A23, A24, A15, Th6, TREES_2:31; :: thesis: