let S be Language; :: thesis: for s being low-compounding Element of S
for T, U being |.(ar b₁).| -element Element of (AllTermsOf S) * st s is termal holds
{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable
let s be low-compounding Element of S; :: thesis: for T, U being |.(ar s).| -element Element of (AllTermsOf S) * st s is termal holds
{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable
set m = |.(ar s).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
let T, U be |.(ar s).| -element Element of (AllTermsOf S) * ; :: thesis: ( s is termal implies {[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable )
assume s is termal ; :: thesis: {[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable
then reconsider ss = s as termal Element of S ;
reconsider t1 = ss -compound T, t2 = ss -compound U as termal string of S ;
reconsider conclusion = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as wff string of S ;
reconsider seqt = [(PairWiseEq (T,U)),conclusion] as Element of S -sequents by Def2;
reconsider Seqts = {} as Subset of (S -sequents) by XBOOLE_1:2;
seqt Rule3d Seqts ;
then [Seqts,seqt] in P#3d S by Def39;
then seqt in (R#3d S) . Seqts by Lm27;
hence {[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable by Lm20, ZFMISC_1:31; :: thesis: verum