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:34;
A3:
<*T*> = {} ^ <*T*>
by FINSEQ_1:34;
A4:
<*T1,T2*> ^ {} = <*T1,T2*>
by FINSEQ_1:34;
A5:
<*T1,T*> ^ {} = <*T1,T*>
by FINSEQ_1:34;
A6:
len <*T1*> = 1
by FINSEQ_1:40;
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, Th57; verum