let A, B, A1, B1 be MP-wff; :: thesis: ( A '&' B = A1 '&' B1 implies ( A = A1 & B = B1 ) )
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: ( A = A1 & B = B1 )
A2: not <*0 *>,<*1*> are_c=-comparable by TREES_1:23;
A3: not <*1*> is_a_proper_prefix_of <*0 *> by TREES_1:89;
A4: ( <*0 *> in elementary_tree 2 & <*1*> in elementary_tree 2 ) by TREES_1:55;
A5: dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 by FUNCOP_1:19;
then A6: <*0 *> in (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*1*>,(dom B) by A3, A4, TREES_1:def 12;
A7: ( dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) = (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom A) & dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1) = (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom A1) ) by A4, A5, TREES_2:def 12;
not <*0 *> is_a_proper_prefix_of <*1*> by TREES_1:89;
then A8: ( <*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) & <*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1) ) by A4, A5, A7, TREES_1:def 12;
then A9: ( dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)) with-replacement <*1*>,(dom B) & dom (A1 '&' B1) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1)) with-replacement <*1*>,(dom B1) ) by TREES_2:def 12;

now

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

proof

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

now

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: s in dom B1

hence s in dom B1 by TREES_1:47; :: thesis: verum

end;

suppose s <> {} ; :: thesis: s in dom B1

then <*1*> is_a_proper_prefix_of <*1*> ^ s by TREES_1:33;
then ex w being FinSequence of NAT st
( w in dom B1 & <*1*> ^ s = <*1*> ^ w ) by A8, A9, A10, TREES_1:def 12;
hence s in dom B1 by FINSEQ_1:46; :: thesis: verum

end;

end;

end;

hence s in dom B1 ; :: thesis: verum

end;

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

now

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: s in dom B

hence s in dom B by TREES_1:47; :: thesis: verum

end;

suppose s <> {} ; :: thesis: s in dom B

then <*1*> is_a_proper_prefix_of <*1*> ^ s by TREES_1:33;
then ex w being FinSequence of NAT st
( w in dom B & <*1*> ^ s = <*1*> ^ w ) by A8, A9, A11, TREES_1:def 12;
hence s in dom B by FINSEQ_1:46; :: thesis: verum

end;

end;

end;

hence s in dom B ; :: thesis: verum

end;

then A12: dom B = dom B1 by TREES_2:def 1;
A13: dom (A '&' B) = ((dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*1*>,(dom B)) with-replacement <*0 *>,(dom A) by A2, A4, A5, A7, A9, TREES_2:10;
dom (A1 '&' B1) = ((dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*1*>,(dom B)) with-replacement <*0 *>,(dom A1) by A2, A4, A5, A7, A9, A12, TREES_2:10;
then A14: dom A = dom A1 by A1, A6, A13, Th15;
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: ( s in dom B implies B . s = B1 . s )
assume s in dom B ; :: thesis: B . s = B1 . s
then A16: <*1*> ^ s in dom (A1 '&' B1) by A1, A8, A9, TREES_1:def 12;
A17: <*1*> is_a_prefix_of <*1*> ^ s by TREES_1:8;
then consider w being FinSequence of NAT such that
A18: ( w in dom B1 & <*1*> ^ s = <*1*> ^ w & (A1 '&' B1) . (<*1*> ^ s) = B1 . w ) by A8, A9, A16, TREES_2:def 12;
A19: s = w by A18, FINSEQ_1:46;
ex u being FinSequence of NAT st
( u in dom B & <*1*> ^ s = <*1*> ^ u & (A '&' B) . (<*1*> ^ s) = B . u ) by A1, A8, A9, A16, A17, TREES_2:def 12;
hence B . s = B1 . s by A1, A18, A19, FINSEQ_1:46; :: thesis: verum

end;

then A20: B = B1 by A12, TREES_2:33;
for s being FinSequence of NAT st s in dom A holds
A . s = A1 . s

proof

let s be FinSequence of NAT ; :: thesis: ( s in dom A implies A . s = A1 . s )
assume A21: s in dom A ; :: thesis: A . s = A1 . s
then A22: <*0 *> ^ s in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) by A4, A5, A7, TREES_1:def 12;
not <*1*> is_a_proper_prefix_of <*0 *> ^ s by Th5;
then A23: <*0 *> ^ s in dom (A '&' B) by A8, A9, A22, TREES_1:def 12;

now

given w being FinSequence of NAT such that A24: ( w in dom B & <*0 *> ^ s = <*1*> ^ w & (A '&' B) . (<*0 *> ^ s) = B . w ) ; :: thesis: contradiction
<*0 *> is_a_prefix_of <*1*> ^ w by A24, TREES_1:8;
hence contradiction by TREES_1:87; :: thesis: verum

end;

then A25: ( not <*1*> is_a_prefix_of <*0 *> ^ s & (A '&' B) . (<*0 *> ^ s) = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) . (<*0 *> ^ s) ) by A8, A9, A23, TREES_2:def 12;
A26: <*0 *> is_a_prefix_of <*0 *> ^ s by TREES_1:8;
then 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 A4, A5, A7, A22, TREES_2:def 12;
then A27: A . s = (A1 '&' B) . (<*0 *> ^ s) by A1, A20, A25, FINSEQ_1:46;
A28: <*0 *> ^ s in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1) by A4, A5, A7, A14, A21, TREES_1:def 12;

now

given w being FinSequence of NAT such that A29: ( w in dom B1 & <*0 *> ^ s = <*1*> ^ w & (A1 '&' B1) . (<*0 *> ^ s) = B1 . w ) ; :: thesis: contradiction
<*0 *> is_a_prefix_of <*1*> ^ w by A29, TREES_1:8;
hence contradiction by TREES_1:87; :: thesis: verum

end;

then A30: ( not <*1*> is_a_prefix_of <*0 *> ^ s & (A1 '&' B1) . (<*0 *> ^ s) = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1) . (<*0 *> ^ s) ) by A1, A8, A9, A23, TREES_2:def 12;
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 A4, A5, A7, A26, A28, TREES_2:def 12;
hence A . s = A1 . s by A20, A27, A30, FINSEQ_1:46; :: thesis: verum

end;

hence ( A = A1 & B = B1 ) by A12, A14, A15, TREES_2:33; :: thesis: verum