let X be set ; :: thesis: for S being Language
for U being non empty set
for I1, I2 being b1,b2 -interpreter-like Function st I1 | X = I2 | X holds
() | (X *) = () | (X *)

let S be Language; :: thesis: for U being non empty set
for I1, I2 being S,b1 -interpreter-like Function st I1 | X = I2 | X holds
() | (X *) = () | (X *)

let U be non empty set ; :: thesis: for I1, I2 being S,U -interpreter-like Function st I1 | X = I2 | X holds
() | (X *) = () | (X *)

set T = S -termsOfMaxDepth ;
set O = OwnSymbolsOf S;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set L = LettersOf S;
set F = S -firstChar ;
set C = S -multiCat ;
let I1, I2 be S,U -interpreter-like Function; :: thesis: ( I1 | X = I2 | X implies () | (X *) = () | (X *) )
set E1 = I1 -TermEval ;
set E2 = I2 -TermEval ;
set I11 = I1 | X;
set I22 = I2 | X;
assume A1: I1 | X = I2 | X ; :: thesis: () | (X *) = () | (X *)
then A2: ( dom () = AllTermsOf S & dom () = AllTermsOf S & I1 | X = I2 | X ) by FUNCT_2:def 1;
defpred S1[ Nat] means () | ((X *) /\ (() . \$1)) = () | ((X *) /\ (() . \$1));
A3: S1[ 0 ]
proof
set d = (X *) /\ ();
( (S -termsOfMaxDepth) . 0 c= AllTermsOf S & (X *) /\ () c= () . 0 ) by FOMODEL1:2;
then reconsider dd = (X *) /\ () as Subset of () by XBOOLE_1:1;
A4: ( dom (() | dd) = (X *) /\ () & dom (() | dd) = (X *) /\ () ) by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom (() | ((X *) /\ ())) holds
(() | ((X *) /\ ())) . x = (() | ((X *) /\ ())) . x
let x be object ; :: thesis: ( x in dom (() | ((X *) /\ ())) implies (() | ((X *) /\ ())) . x = (() | ((X *) /\ ())) . x )
assume A5: x in dom (() | ((X *) /\ ())) ; :: thesis: (() | ((X *) /\ ())) . x = (() | ((X *) /\ ())) . x
reconsider dd = dd as non empty Subset of () by A5;
reconsider xd = x as Element of dd by A5;
reconsider t = x as 0 -termal string of S by ;
set o = () . t;
set ST = SubTerms t;
reconsider XX = X as non empty set by A5;
reconsider tx = x as non empty Element of XX * by A5, A4;
{(tx . 1)} \ XX = {} ;
then tx . 1 in XX by ZFMISC_1:60;
then reconsider oo = () . t as Element of XX by FOMODEL0:6;
( ((I1 | X) . oo) \+\ (I1 . oo) = {} & ((I2 | X) . oo) \+\ (I2 . oo) = {} & ((() | dd) . xd) \+\ (() . xd) = {} & ((() | dd) . xd) \+\ (() . xd) = {} ) ;
then A6: ( (I1 | X) . (() . t) = I1 . (() . t) & (I2 | X) . (() . t) = I2 . (() . t) & (() | ((X *) /\ ())) . x = () . x & (() | ((X *) /\ ())) . x = () . x ) by FOMODEL0:29;
hence (() | ((X *) /\ ())) . x = (I1 . (() . t)) . (() * ()) by Th21
.= (I2 . (() . t)) . (() * ()) by A1, A6
.= (() | ((X *) /\ ())) . x by ;
:: thesis: verum
end;
hence S1[ 0 ] by ; :: thesis: verum
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set d = (X *) /\ (() . n);
set D = (X *) /\ (() . (n + 1));
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;
assume A8: S1[n] ; :: thesis: S1[n + 1]
( (X *) /\ (() . (n + 1)) c= () . NN & (X *) /\ (() . n) c= () . nn & () . nn c= AllTermsOf S & () . NN c= AllTermsOf S ) by FOMODEL1:2;
then reconsider DD = (X *) /\ (() . (n + 1)), dd = (X *) /\ (() . n) as Subset of () by XBOOLE_1:1;
A9: ( dom (() | dd) = (X *) /\ (() . n) & dom (() | dd) = (X *) /\ (() . n) & dom (() | DD) = (X *) /\ (() . (n + 1)) & dom (() | DD) = (X *) /\ (() . (n + 1)) ) by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom (() | ((X *) /\ (() . (n + 1)))) holds
(() | ((X *) /\ (() . (n + 1)))) . x = (() | ((X *) /\ (() . (n + 1)))) . x
let x be object ; :: thesis: ( x in dom (() | ((X *) /\ (() . (n + 1)))) implies (() | ((X *) /\ (() . (n + 1)))) . x = (() | ((X *) /\ (() . (n + 1)))) . x )
assume A10: x in dom (() | ((X *) /\ (() . (n + 1)))) ; :: thesis: (() | ((X *) /\ (() . (n + 1)))) . x = (() | ((X *) /\ (() . (n + 1)))) . x
reconsider t = x as nn + 1 -termal string of S by ;
reconsider XX = X as non empty set by A10;
reconsider DD = DD as non empty Subset of () by A10;
reconsider tx = x as non empty Element of XX * by ;
reconsider dx = x as Element of DD by A10;
set o = () . t;
set m = |.(ar (() . t)).|;
{(tx . 1)} \ XX = {} ;
then tx . 1 in XX by ZFMISC_1:60;
then reconsider oo = () . t as Element of XX by FOMODEL0:6;
reconsider r = rng t as Subset of X by ;
r * c= X * ;
then reconsider newords = (rng t) * as non empty Subset of (X *) ;
reconsider ST = SubTerms t as newords -valued |.(ar (() . t)).| -element FinSequence ;
( ((I1 | X) . oo) \+\ (I1 . oo) = {} & ((I2 | X) . oo) \+\ (I2 . oo) = {} ) ;
then A11: ( (I1 | X) . oo = I1 . oo & (I2 | X) . oo = I2 . oo ) by FOMODEL0:29;
( (((I1 -TermEval) | DD) . dx) \+\ (() . dx) = {} & ((() | DD) . dx) \+\ (() . dx) = {} ) ;
then A12: ( ((I1 -TermEval) | ((X *) /\ (() . (n + 1)))) . x = () . x & (() | ((X *) /\ (() . (n + 1)))) . x = () . x ) by FOMODEL0:29;
( rng ST c= () . nn & rng ST c= X * ) by RELAT_1:def 19;
then A13: ( ((I1 -TermEval) | ((X *) /\ (() . n))) * ST = () * ST & (() | ((X *) /\ (() . n))) * ST = () * ST ) by ;
then (I1 . (() . t)) . ((() | ((X *) /\ (() . n))) * ST) = () . t by Th21;
hence ((I1 -TermEval) | ((X *) /\ (() . (n + 1)))) . x = (() | ((X *) /\ (() . (n + 1)))) . x by A12, A8, A1, A11, A13, Th21; :: thesis: verum
end;
hence S1[n + 1] by ; :: thesis: verum
end;
A14: for m being Nat holds S1[m] from NAT_1:sch 2(A3, A7);
set f1 = () | (X *);
set f2 = () | (X *);
A15: ( dom (() | (X *)) = (X *) /\ () & dom (() | (X *)) = (X *) /\ () ) by ;
now :: thesis: for x being object st x in dom (() | (X *)) holds
(() | (X *)) . x = (() | (X *)) . x
let x be object ; :: thesis: ( x in dom (() | (X *)) implies (() | (X *)) . x = (() | (X *)) . x )
assume A16: x in dom (() | (X *)) ; :: thesis: (() | (X *)) . x = (() | (X *)) . x
reconsider D = (X *) /\ () as non empty Subset of () by ;
reconsider t = x as termal string of S by ;
set m = Depth t;
reconsider t = t as Depth t -termal string of S by FOMODEL1:def 40;
A17: ( t in X * & t in () . () ) by ;
reconsider Dm = (X *) /\ (() . ()) as non empty set by ;
reconsider tt = t as Element of Dm by ;
reconsider xx = x as Element of X * by A16;
set g1 = () | Dm;
set g2 = () | Dm;
( (((I1 -TermEval) | (X *)) . xx) \+\ (() . xx) = {} & ((() | (X *)) . xx) \+\ (() . xx) = {} & ((() | Dm) . tt) \+\ (() . tt) = {} & ((() | Dm) . tt) \+\ (() . tt) = {} ) ;
then ( ((I1 -TermEval) | (X *)) . x = () . x & (() | (X *)) . x = () . x & (() | Dm) . x = () . x & (() | Dm) . x = () . x ) by FOMODEL0:29;
hence ((I1 -TermEval) | (X *)) . x = (() | (X *)) . x by A14; :: thesis: verum
end;
hence (I1 -TermEval) | (X *) = () | (X *) by ; :: thesis: verum