let A, B be MP-wff; :: thesis: (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff
reconsider d = <*0*> as Element of elementary_tree 2 by TREES_1:28;
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
set x = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);
A1: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:3;
reconsider db = dom B as finite Tree ;
reconsider da = dom A as finite Tree ;
<*0*> in elementary_tree 2 by TREES_1:28;
then A2: <*0*> in dom ((elementary_tree 2) --> [2,0]) by FUNCOP_1:13;
then @ (((elementary_tree 2) --> [2,0]),<*0*>,A) = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) by Def7;
then reconsider y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) as DecoratedTree of [:NAT,NAT:] ;
A3: dom y = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A2, TREES_2:def 11;
dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 by FUNCOP_1:13;
then dom y = (elementary_tree 2) with-replacement (d,da) by TREES_2:def 11;
then reconsider dy = dom y as finite Tree ;
<*1*> in elementary_tree 2 by TREES_1:28;
then A4: <*1*> in dom ((elementary_tree 2) --> [2,0]) by FUNCOP_1:13;
then A5: <*1*> in dom y by A2, A3, A1, TREES_1:def 9;
reconsider d1 = <*1*> as Element of dy by A2, A3, A4, A1, TREES_1:def 9;
( dom ((((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B)) = dy with-replacement (d1,db) & @ (y,<*1*>,B) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) ) by A5, Def7, TREES_2:def 11;
then reconsider x = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) as finite DecoratedTree of [:NAT,NAT:] by Lm2;
A6: dom x = (dom y) with-replacement (<*1*>,(dom B)) by A5, 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 2) --> [2,0];
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 & ( 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 <*1*> is_a_prefix_of v & x . v = y . v ) or ex s being FinSequence of NAT st
( s in dom B & v = <*1*> ^ s & x . v = B . s ) ) by A5, A6, TREES_2:def 11;

suppose A7: ( not <*1*> is_a_prefix_of v & x . v = y . v ) ; :: 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] ) )

then A8: for s being FinSequence of NAT holds
( not s in dom B or not v = <*1*> ^ s ) by TREES_1:1;
then A9: v in (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A3, A5, A6, TREES_1:def 9;

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 & y . v = ((elementary_tree 2) --> [2,0]) . v ) or ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & y . v = A . s ) ) by A2, A9, TREES_2:def 11;

suppose A10: ( not <*0*> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0]) . 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] ) )

A11: dom ((elementary_tree 2) --> [2,0]) = {{},<*0*>,<*1*>} by FUNCOP_1:13, TREES_1:53;
A12: for s being FinSequence of NAT holds
( not s in dom A or not v = <*0*> ^ s ) by A10, TREES_1:1;
then A13: v in dom ((elementary_tree 2) --> [2,0]) by A2, A9, TREES_1:def 9;
then A14: v = {} by A7, A10, A11, ENUMSET1:def 1;
reconsider v9 = v as Element of dom ((elementary_tree 2) --> [2,0]) by A2, A9, A12, TREES_1:def 9;
A15: succ v = succ v9

proof

reconsider v99 = v as Element of dom y by A5, A6, A8, TREES_1:def 9;
succ v99 = succ v9 by A2, A3, A14, Lm1, Th8;
hence succ v = succ v9 by A5, A6, A14, Lm1, Th8; :: thesis: verum

end;

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

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

proof

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

end;

assume x in {<*0*>,<*1*>} ; :: thesis: x in succ v9
then A19: ( x = <*0*> or x = <*1*> ) by TARSKI:def 2;

now :: thesis: x in succ v9

per cases ( x = v9 ^ <*0*> or x = v9 ^ <*1*> ) by A14, A19, FINSEQ_1:34;

suppose A20: x = v9 ^ <*0*> ; :: thesis: x in succ v9

then v9 ^ <*0*> in dom ((elementary_tree 2) --> [2,0]) by A11, A19, ENUMSET1:def 1;
then x in { (v9 ^ <*n*>) where n is Nat : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by A20;
hence x in succ v9 by TREES_2:def 5; :: thesis: verum

end;

suppose A21: x = v9 ^ <*1*> ; :: thesis: x in succ v9

then v9 ^ <*1*> in dom ((elementary_tree 2) --> [2,0]) by A11, A19, ENUMSET1:def 1;
then x in { (v9 ^ <*n*>) where n is Nat : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by A21;
hence x in succ v9 by TREES_2:def 5; :: thesis: verum

end;

end;

end;

hence x in succ v9 ; :: thesis: verum

end;

then A22: succ v9 = {<*0*>,<*1*>} by TARSKI:2;
<*0*> <> <*1*> by TREES_1:3;
then A23: 2 = card (succ v) by A22, A15, CARD_2:57;
hence branchdeg v <= 2 by 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] ) )
v in elementary_tree 2 by A13;
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 A7, A10, A23, FUNCOP_1:7, TREES_2:def 12; :: thesis: verum

end;

suppose ex s being FinSequence of NAT st
( s in dom A & v = <*0*> ^ s & y . 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
A24: s in dom A and
A25: v = <*0*> ^ s and
A26: y . v = A . s ;
reconsider s = s as Element of dom A by A24;
succ v, succ s are_equipotent

proof

reconsider v9 = v as Element of dom y by A5, A6, A8, TREES_1:def 9;
succ v9, succ s are_equipotent by A2, A3, A25, TREES_2:37;
hence succ v, succ s are_equipotent by A5, A6, A25, Th1, Th9; :: thesis: verum

end;

then card (succ v) = card (succ s) by CARD_1:5;
then A27: branchdeg v = card (succ s) by TREES_2:def 12;
A28: branchdeg s <= 2 by Def5;
hence branchdeg v <= 2 by A27, 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] ) )
A29: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5;
A30: ( 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 A7, A26, A28, A29, A30, A27, 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;

suppose ex s being FinSequence of NAT st
( s in dom B & v = <*1*> ^ s & x . v = B . s ) ; :: 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] ) )

then consider s being FinSequence of NAT such that
A31: s in dom B and
A32: v = <*1*> ^ s and
A33: x . v = B . s ;
reconsider s = s as Element of dom B by A31;
succ v, succ s are_equipotent by A5, A6, A32, TREES_2:37;
then card (succ v) = card (succ s) by CARD_1:5;
then A34: branchdeg v = card (succ s) by TREES_2:def 12;
A35: ( branchdeg s = 2 implies B . s = [2,0] ) by Def5;
A36: ( not branchdeg s = 1 or B . s = [1,0] or B . s = [1,1] ) by Def5;
A37: ( not branchdeg s = 0 or B . s = [0,0] or ex m being Nat st B . s = [3,m] ) by Def5;
branchdeg s <= 2 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 A33, A37, A36, A35, A34, 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 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Def5; :: thesis: verum