let A, A1, B, 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: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;
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 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;
verum
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 ;
( 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 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;
verum
end;
hence
( A = A1 & B = B1 )
by A1, A5, A14, A23, A24, A15, Th6, TREES_2:31; verum