let X, x1, x2 be set ; :: thesis:
let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
let s be low-compounding Element of S; :: thesis:
set n = |.(ar s).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set f = S -cons ;
set SS = AllSymbolsOf S;
set R = (X,D) -termEq ;
set SS = AllSymbolsOf S;
assume A1: X is D -expanded ; :: thesis:
assume [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) ; :: thesis:
then consider p, q being Element of |.(ar s).| -tuples_on (AllTermsOf S) such that
A2: ( [x1,x2] = [p,q] & ( for i being set st i in Seg |.(ar s).| holds
[(p . i),(q . i)] in (X,D) -termEq ) ) ;
A3: ( p = x1 & q = x2 ) by A2, XTUPLE_0:1;
reconsider T1 = x1, T2 = x2 as Element of |.(ar s).| -tuples_on (AllTermsOf S) by A2, XTUPLE_0:1;
reconsider T11 = T1, T22 = T2 as |.(ar s).| -element Element of (AllTermsOf S) * by FINSEQ_1:def 11;
take T = T11; :: thesis:
take U = T22; :: thesis:
thus ( T = x1 & U = x2 ) ; :: thesis:
set Z = PairWiseEq (T,U);
( T1 is Element of Funcs ((Seg |.(ar s).|),(AllTermsOf S)) & T2 is Element of Funcs ((Seg |.(ar s).|),(AllTermsOf S)) ) by FOMODEL0:11;
then reconsider T111 = T1, T222 = T2 as Function of (Seg |.(ar s).|),(AllTermsOf S) ;

now :: thesis:

let z be object ; :: thesis:
assume z in PairWiseEq (T,U) ; :: thesis:
then consider j being Element of Seg |.(ar s).|, TT, UU being Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) such that
A4: ( z = (<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j) & TT = T11 & UU = T22 ) ;
reconsider t11 = T111 . j, t22 = T222 . j as Element of AllTermsOf S ;
reconsider t1 = t11, t2 = t22 as termal string of S ;
[(T111 . j),(T222 . j)] in (X,D) -termEq by A2, A3;
then (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable by Lm23;
then {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} c= X by A1;
hence z in X by A4, ZFMISC_1:31; :: thesis:

end;

hence PairWiseEq (T,U) c= X by TARSKI:def 3; :: thesis: