now :: thesis: for A being set st A in (((MSVars C),(a_Term C)) variables_in) .: (adjs T) holds
A is finite
let A be set ; :: thesis: ( A in (((MSVars C),(a_Term C)) variables_in) .: (adjs T) implies A is finite )
assume A in (((MSVars C),(a_Term C)) variables_in) .: (adjs T) ; :: thesis: A is finite
then consider x being object such that
A1: x in Union the Sorts of (Free (C,(MSVars C))) and
x in adjs T and
A2: A = (((MSVars C),(a_Term C)) variables_in) . x by FUNCT_2:64;
reconsider x = x as expression of C by A1;
A = (C variables_in x) . (a_Term C) by A2, Def45;
hence A is finite ; :: thesis: verum
end;
then union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T)) is finite by FINSET_1:7;
hence variables_in T is finite ; :: thesis: verum