let S be Language; :: thesis: R#3d S is Correct

now :: thesis: for X being set st X is S -correct holds
(R#3d S) . X is S -correct

set f = R#3d S;
set R = P#3d S;
set Q = S -sequents ;
set E = TheEqSymbOf S;
set N = TheNorSymbOf S;
set FF = AllFormulasOf S;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
let X be set ; :: thesis: ( X is S -correct implies (R#3d S) . X is S -correct )
assume A1: X is S -correct ; :: thesis: (R#3d S) . X is S -correct

now :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S
for x being b₂ -satisfied set
for psi being wff string of S st [x,psi] in (R#3d S) . X holds
I -TruthEval psi = 1

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S
for x being b₁ -satisfied set
for psi being wff string of S st [x,psi] in (R#3d S) . X holds
I -TruthEval psi = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R#3d S) . X holds
I -TruthEval psi = 1
let x be I -satisfied set ; :: thesis: for psi being wff string of S st [x,psi] in (R#3d S) . X holds
I -TruthEval psi = 1
let psi be wff string of S; :: thesis: ( [x,psi] in (R#3d S) . X implies I -TruthEval psi = 1 )
set s = [x,psi];
set TE = I -TermEval ;
set d = U -deltaInterpreter ;
assume A3: [x,psi] in (R#3d S) . X ; :: thesis: I -TruthEval psi = 1
then A4: ( [x,psi] in S -sequents & [X,[x,psi]] in P#3d S ) by Lm30;
then X in dom (P#3d S) by XTUPLE_0:def 12;
then reconsider Seqts = X as S -correct Subset of (S -sequents) by A1;
reconsider seqt = [x,psi] as Element of S -sequents by A3, Lm30;
seqt Rule3d Seqts by A4, Def39;
then consider r being low-compounding Element of S, T1, T2 being |.(ar r).| -element Element of (AllTermsOf S) * such that
A5: ( r is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg |.(ar r).|, TT1, TT2 is Function of (Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (r -compound T1)) ^ (r -compound T2) ) ;
reconsider t1 = r -compound T1, t2 = r -compound T2 as termal string of S by A5;
( (t1 . 1) \+\ r = {} & (t2 . 1) \+\ r = {} ) ;
then ( t1 . 1 = r & t2 . 1 = r ) by FOMODEL0:29;
then A6: ( (S -firstChar) . t1 = r & (S -firstChar) . t2 = r ) by FOMODEL0:6;
then ( SubTerms t1 = T1 & SubTerms t2 = T2 ) by FOMODEL1:def 37;
then A7: ( (I -TermEval) . t1 = (I . r) . ((I -TermEval) * T1) & (I -TermEval) . t2 = (I . r) . ((I -TermEval) * T2) ) by FOMODEL2:21, A6;
reconsider Fam = { ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg |.(ar r).|, TT1, TT2 is Function of (Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } null {} as Subset of x by A5;

now :: thesis: ( len ((I -TermEval) * T2) = len ((I -TermEval) * T1) & ( for k being Nat st 1 <= k & k <= len ((I -TermEval) * T1) holds
((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k ) )

set p = (I -TermEval) * T1;
set q = (I -TermEval) * T2;
len ((I -TermEval) * T1) = |.(ar r).| by CARD_1:def 7;
hence len ((I -TermEval) * T2) = len ((I -TermEval) * T1) by CARD_1:def 7; :: thesis: for k being Nat st 1 <= k & k <= len ((I -TermEval) * T1) holds
((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len ((I -TermEval) * T1) implies ((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k )
assume A8: ( 1 <= k & k <= len ((I -TermEval) * T1) ) ; :: thesis: ((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k
then A9: ( 1 <= k & k <= |.(ar r).| ) by CARD_1:def 7;
then reconsider kk = k as Element of Seg |.(ar r).| by FINSEQ_1:1;
k - k <= |.(ar r).| - k by A9, XREAL_1:9;
then reconsider h = |.(ar r).| - k as Nat ;
reconsider k1 = k as non zero Nat by A8;
( dom (T1 null 0) = Seg (|.(ar r).| + 0) & rng T1 c= ((AllSymbolsOf S) *) \ {{}} & dom (T2 null 0) = Seg (|.(ar r).| + 0) & rng T2 c= ((AllSymbolsOf S) *) \ {{}} ) by PARTFUN1:def 2, RELAT_1:def 19;
then ( T1 is Element of Funcs ((Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}})) & T2 is Element of Funcs ((Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}})) ) by FUNCT_2:def 2;
then reconsider TT1 = T1, TT2 = T2 as Function of (Seg |.(ar r).|),(((AllSymbolsOf S) *) \ {{}}) ;
( T1 is k1 + h -element & T2 is k1 + h -element ) ;
then ( {(T1 . k1)} \ (AllTermsOf S) = {} & {(T2 . k1)} \ (AllTermsOf S) = {} ) ;
then ( T1 . k in AllTermsOf S & T2 . k in AllTermsOf S ) by ZFMISC_1:60;
then reconsider t1 = T1 . k, t2 = T2 . k as termal string of S ;
reconsider z = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as 0wff string of S ;
( ((I -TermEval) . (TT1 . kk)) \+\ (((I -TermEval) * TT1) . kk) = {} & ((I -TermEval) . (TT2 . kk)) \+\ (((I -TermEval) * TT2) . kk) = {} ) ;
then A10: ( (I -TermEval) . (TT1 . kk) = ((I -TermEval) * TT1) . kk & (I -TermEval) . (TT2 . kk) = ((I -TermEval) * TT2) . kk ) by FOMODEL0:29;
set ST = <*t1,t2*>;
(<*(TheEqSymbOf S)*> ^ (TT1 . kk)) ^ (TT2 . kk) in Fam ;
then I -TruthEval z = 1 by FOMODEL2:def 42;
hence ((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k by A10, Lm54; :: thesis: verum

end;

then (I -TermEval) . t1 = (I -TermEval) . t2 by A7, FINSEQ_1:14;
then ( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 & psi = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 ) by Lm54, A5;
hence I -TruthEval psi = 1 ; :: thesis: verum

end;

hence (R#3d S) . X is S -correct ; :: thesis: verum

end;

hence R#3d S is Correct ; :: thesis: verum