let T, T1, T2 be Tree; ( (tree T1,T2) with-replacement <*0 *>,T = tree T,T2 & (tree T1,T2) with-replacement <*1*>,T = tree T1,T )
A1:
len {} = 0
;
A2:
<*T1*> = {} ^ <*T1*>
by FINSEQ_1:47;
A3:
<*T*> = {} ^ <*T*>
by FINSEQ_1:47;
A4:
<*T1,T2*> ^ {} = <*T1,T2*>
by FINSEQ_1:47;
A5:
<*T1,T*> ^ {} = <*T1,T*>
by FINSEQ_1:47;
A6:
len <*T1*> = 1
by FINSEQ_1:57;
A7:
<*T1,T2*> = <*T1*> ^ <*T2*>
by FINSEQ_1:def 9;
A8:
<*T1,T*> = <*T1*> ^ <*T*>
by FINSEQ_1:def 9;
<*T,T2*> = <*T*> ^ <*T2*>
by FINSEQ_1:def 9;
hence
( (tree T1,T2) with-replacement <*0 *>,T = tree T,T2 & (tree T1,T2) with-replacement <*1*>,T = tree T1,T )
by A1, A2, A3, A4, A5, A6, A7, A8, Th60; verum