set P = PairWiseEq (T1,T2);
set SS = AllSymbolsOf S;
set E = TheEqSymbOf S;
set AT = AllTermsOf S;
set AF = AllFormulasOf S;
now for x being object st x in PairWiseEq (T1,T2) holds
x in AllFormulasOf Slet x be
object ;
( x in PairWiseEq (T1,T2) implies x in AllFormulasOf S )assume
x in PairWiseEq (
T1,
T2)
;
x in AllFormulasOf Sthen consider j being
Element of
Seg m,
T11,
T22 being
Function of
(Seg m),
(((AllSymbolsOf S) *) \ {{}}) such that A1:
(
x = (<*(TheEqSymbOf S)*> ^ (T11 . j)) ^ (T22 . j) &
T11 = T1 &
T22 = T2 )
;
m -tuples_on (AllTermsOf S) = Funcs (
(Seg m),
(AllTermsOf S))
by FOMODEL0:11;
then
(
T1 is
Element of
Funcs (
(Seg m),
(AllTermsOf S)) &
T2 is
Element of
Funcs (
(Seg m),
(AllTermsOf S)) )
by FOMODEL0:16;
then reconsider T111 =
T1,
T222 =
T2 as
Function of
(Seg m),
(AllTermsOf S) ;
(
T111 . j is
Element of
AllTermsOf S &
T222 . j is
Element of
AllTermsOf S )
;
then reconsider t1 =
T111 . j,
t2 =
T222 . j as
string of
S ;
reconsider w =
(<*(TheEqSymbOf S)*> ^ t1) ^ t2 as
0 -wff string of
S ;
w in AllFormulasOf S
;
hence
x in AllFormulasOf S
by A1;
verum end;
hence
PairWiseEq (T1,T2) is Subset of (AllFormulasOf S)
by TARSKI:def 3; verum