per cases
( ( TM1 is empty & TM2 is empty ) or not TM1 is empty or not TM2 is empty )
;

end;

suppose
( TM1 is empty & TM2 is empty )
; :: thesis: [:TM1,TM2:] is with_finite_small_inductive_dimension

end;

end;

suppose
( not TM1 is empty or not TM2 is empty )
; :: thesis: [:TM1,TM2:] is with_finite_small_inductive_dimension

end;

end;