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

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

hence [:TM1,TM2:] is with_finite_small_inductive_dimension ; :: thesis: verum

end;

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

hence [:TM1,TM2:] is with_finite_small_inductive_dimension by Lm5; :: thesis: verum

end;

end;