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;