let T1, T2 be Tree; :: thesis: (^ T1) with-replacement (<*0*>,T2) = ^ T2
A1: len {} = 0 ;
A2: <*T1*> = {} ^ <*T1*> by FINSEQ_1:34;
A3: <*T2*> = {} ^ <*T2*> by FINSEQ_1:34;
A4: <*T1*> = <*T1*> ^ {} by FINSEQ_1:34;
<*T2*> = <*T2*> ^ {} by FINSEQ_1:34;
hence (^ T1) with-replacement (<*0*>,T2) = ^ T2 by A1, A2, A3, A4, Th57; :: thesis: verum