let A be MP-wff; :: thesis: ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff
reconsider d = <*0*> as Element of elementary_tree 1 by TREES_1:28;
set x = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A);
<*0*> in elementary_tree 1 by TREES_1:28;
then A1: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13;
then dom (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by TREES_2:def 11;
then A2: dom (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A)) = (elementary_tree 1) with-replacement (d,(dom A)) by FUNCOP_1:13;
@ (((elementary_tree 1) --> [1,1]),<*0*>,A) = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) by A1, Def7;
then reconsider x = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) as finite DecoratedTree of [:NAT,NAT:] by A2, Lm2;
A3: dom x = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by A1, TREES_2:def 11;
for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )

proof

set e = (elementary_tree 1) --> [1,1];
let v be Element of dom x; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )

now :: thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )

per cases ( ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . v ) or ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & x . v = A . s ) ) by A1, A3, TREES_2:def 11;

suppose A4: ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . v ) ; :: thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )

A5: dom ((elementary_tree 1) --> [1,1]) = {{},<*0*>} by FUNCOP_1:13, TREES_1:51;
A6: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0*> ^ s ) by A4, TREES_1:1;
then A7: v in dom ((elementary_tree 1) --> [1,1]) by A1, A3, TREES_1:def 9;
then A8: v = {} by A4, A5, TARSKI:def 2;
reconsider v9 = v as Element of dom ((elementary_tree 1) --> [1,1]) by A1, A3, A6, TREES_1:def 9;

now :: thesis: for x being object holds
( ( x in succ v9 implies x in {<*0*>} ) & ( x in {<*0*>} implies x in succ v9 ) )

let x be object ; :: thesis: ( ( x in succ v9 implies x in {<*0*>} ) & ( x in {<*0*>} implies x in succ v9 ) )
thus ( x in succ v9 implies x in {<*0*>} ) :: thesis: ( x in {<*0*>} implies x in succ v9 )

proof

assume x in succ v9 ; :: thesis: x in {<*0*>}
then x in { (v9 ^ <*n*>) where n is Nat : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by TREES_2:def 5;
then consider n being Nat such that
A9: x = v9 ^ <*n*> and
A10: v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) ;
<*n*> in dom ((elementary_tree 1) --> [1,1]) by A8, A10, FINSEQ_1:34;
then A11: ( <*n*> = {} or <*n*> = <*0*> ) by A5, TARSKI:def 2;
x = <*n*> by A8, A9, FINSEQ_1:34;
hence x in {<*0*>} by A11, TARSKI:def 1; :: thesis: verum

end;

assume x in {<*0*>} ; :: thesis: x in succ v9
then A12: x = <*0*> by TARSKI:def 1;
then A13: x = v9 ^ <*0*> by A8, FINSEQ_1:34;
then v9 ^ <*0*> in dom ((elementary_tree 1) --> [1,1]) by A5, A12, TARSKI:def 2;
then x in { (v9 ^ <*n*>) where n is Nat : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by A13;
hence x in succ v9 by TREES_2:def 5; :: thesis: verum

end;

then A14: succ v9 = {<*0*>} by TARSKI:2;
succ v = succ v9 by A1, A3, A8, Lm1, Th8;
then 1 = card (succ v) by A14, CARD_1:30;
then A15: branchdeg v = 1 by TREES_2:def 12;
hence branchdeg v <= 2 ; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
v in elementary_tree 1 by A7;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A4, A15, FUNCOP_1:7; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & x . v = A . s ) ; :: thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )

then consider s being FinSequence of NAT such that
A16: s in dom A and
A17: v = <*0*> ^ s and
A18: x . v = A . s ;
reconsider s = s as Element of dom A by A16;
succ v, succ s are_equipotent by A1, A3, A17, TREES_2:37;
then card (succ v) = card (succ s) by CARD_1:5;
then A19: branchdeg v = card (succ s) by TREES_2:def 12;
A20: branchdeg s <= 2 by Def5;
hence branchdeg v <= 2 by A19, TREES_2:def 12; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) )
A21: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5;
A22: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5;
( not branchdeg s = 0 or A . s = [0,0] or ex m being Nat st A . s = [3,m] ) by Def5;
hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A18, A20, A21, A22, A19, TREES_2:def 12; :: thesis: verum

end;

end;

end;

hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; :: thesis: verum

end;

hence ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Def5; :: thesis: verum