set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set SS = AllSymbolsOf S;
( T in m -tuples_on (AllTermsOf S) & U in m -tuples_on (AllTermsOf S) ) by FOMODEL0:16;
then ( T is Element of Funcs ((Seg m),(AllTermsOf S)) & U is Element of Funcs ((Seg m),(AllTermsOf S)) ) by FOMODEL0:11;
then reconsider TT = T, UU = U as Function of (Seg m),(AllTermsOf S) ;
deffunc H1( Element of Seg m) -> set = (<*(TheEqSymbOf S)*> ^ (TT . S)) ^ (UU . S);
set IT = { H1(j) where j is Element of Seg m : j in Seg m } ;
A1: Seg m is finite ;
{ H1(j) where j is Element of Seg m : j in Seg m } is finite from FRAENKEL:sch 21(A1);
 then reconsider ITT = { H1(j) where j is Element of Seg m : j in Seg m } as finite set ;
now :: thesis: for x being object st x in PairWiseEq (T,U) holds
x in { H1(j) where j is Element of Seg m : j in Seg m }
let x be object ; :: thesis: ( x in PairWiseEq (T,U) implies x in { H1(j) where j is Element of Seg m : j in Seg m } )
assume x in PairWiseEq (T,U) ; :: thesis: x in { H1(j) where j is Element of Seg m : j in Seg m }
then consider j being Element of Seg m, TTT, UUU being Function of (Seg m),(((AllSymbolsOf S) *) \ {{}}) such that
A2: ( x = (<*(TheEqSymbOf S)*> ^ (TTT . j)) ^ (UUU . j) & TTT = T & UUU = U ) ;
thus x in { H1(j) where j is Element of Seg m : j in Seg m } by A2; :: thesis: verum
end;
then reconsider Y = PairWiseEq (T,U) as Subset of ITT by TARSKI:def 3;
Y is finite ;
hence PairWiseEq (T,U) is finite ; :: thesis: verum