let A, B, A1, B1 be MP-wff; ( 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
; ( A = A1 & B = B1 )
A2:
<*1*> in elementary_tree 2
by TREES_1:55;
A3:
( <*0 *> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 )
by FUNCOP_1:19, TREES_1:55;
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 12;
not <*1*> is_a_proper_prefix_of <*0 *>
by TREES_1:89;
then A5:
<*0 *> in (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*1*>,(dom B)
by A2, A3, TREES_1:def 12;
A6:
not <*0 *> is_a_proper_prefix_of <*1*>
by TREES_1:89;
then A7:
<*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1)
by A2, A3, A4, TREES_1:def 12;
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 12;
then A9:
<*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)
by A2, A3, A6, TREES_1:def 12;
then A10:
dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)) with-replacement <*1*>,(dom B)
by TREES_2:def 12;
A11:
dom (A1 '&' B1) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1)) with-replacement <*1*>,(dom B1)
by A7, TREES_2:def 12;
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 ;
( s in dom B implies B . s = B1 . s )
assume
s in dom B
;
B . s = B1 . s
then A16:
<*1*> ^ s in dom (A1 '&' B1)
by A1, A9, A10, 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
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 12;
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 12;
s = w
by A18, FINSEQ_1:46;
hence
B . s = B1 . s
by A1, A19, A20, FINSEQ_1:46;
verum
end;
then A21:
B = B1
by A14, TREES_2:33;
A22:
not <*0 *>,<*1*> are_c=-comparable
by TREES_1:23;
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:10;
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:10;
then A25:
dom A = dom A1
by A1, A5, A23, Th15;
for s being FinSequence of NAT st s in dom A holds
A . s = A1 . s
proof
let s be
FinSequence of
NAT ;
( s in dom A implies A . s = A1 . s )
assume A26:
s in dom A
;
A . s = A1 . s
then A27:
<*0 *> ^ s in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)
by A3, A8, TREES_1:def 12;
A28:
<*0 *> is_a_prefix_of <*0 *> ^ s
by TREES_1:8;
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 12;
<*0 *> ^ s in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1)
by A3, A4, A25, A26, TREES_1:def 12;
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 12;
not
<*1*> is_a_proper_prefix_of <*0 *> ^ s
by Th5;
then A31:
<*0 *> ^ s in dom (A '&' B)
by A9, A10, A27, TREES_1:def 12;
then
(A '&' B) . (<*0 *> ^ s) = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) . (<*0 *> ^ s)
by A9, A10, A31, TREES_2:def 12;
then A33:
A . s = (A1 '&' B) . (<*0 *> ^ s)
by A1, A21, A29, FINSEQ_1:46;
then
(A1 '&' B1) . (<*0 *> ^ s) = (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A1) . (<*0 *> ^ s)
by A1, A7, A11, A31, TREES_2:def 12;
hence
A . s = A1 . s
by A21, A33, A30, FINSEQ_1:46;
verum
end;
hence
( A = A1 & B = B1 )
by A1, A5, A14, A23, A24, A15, Th15, TREES_2:33; verum