let T, T1, T2 be Tree; :: thesis: ( (tree T1,T2) with-replacement <*0 *>,T = tree T,T2 & (tree T1,T2) with-replacement <*1*>,T = tree T1,T )
( len {} = 0 & <*T1*> = {} ^ <*T1*> & <*T*> = {} ^ <*T*> & <*T1,T2*> ^ {} = <*T1,T2*> & <*T1,T*> ^ {} = <*T1,T*> & len <*T1*> = 1 & <*T1,T2*> = <*T1*> ^ <*T2*> & <*T1,T*> = <*T1*> ^ <*T*> & <*T,T2*> = <*T*> ^ <*T2*> ) by FINSEQ_1:47, FINSEQ_1:57, 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 Th60; :: thesis: verum