let m be Nat; :: thesis: for S being Language
for l1, l2 being literal Element of S holds (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) is Function of ((S -termsOfMaxDepth) . m),((S -termsOfMaxDepth) . m)
let S be Language; :: thesis: for l1, l2 being literal Element of S holds (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) is Function of ((S -termsOfMaxDepth) . m),((S -termsOfMaxDepth) . m)
let l1, l2 be literal Element of S; :: thesis: (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) is Function of ((S -termsOfMaxDepth) . m),((S -termsOfMaxDepth) . m)
set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set g = (AllSymbolsOf S) -concatenation ;
set G = MultPlace ((AllSymbolsOf S) -concatenation);
set e = l1 SubstWith l2;
A1: for t being 0 -termal string of S holds (l1 SubstWith l2) . t in (S -termsOfMaxDepth) . 0

proof

let t be 0 -termal string of S; :: thesis: (l1 SubstWith l2) . t in (S -termsOfMaxDepth) . 0
set l = (S -firstChar) . t;
A2: t = <*((S -firstChar) . t)*> by FOMODEL2:1;
( (S -firstChar) . t = l1 or (S -firstChar) . t <> l1 ) ;
then ( (l1 SubstWith l2) . <*((S -firstChar) . t)*> = <*l2*> or (l1 SubstWith l2) . <*((S -firstChar) . t)*> = <*((S -firstChar) . t)*> ) by FOMODEL0:35;
hence (l1 SubstWith l2) . t in (S -termsOfMaxDepth) . 0 by A2, FOMODEL1:def 33; :: thesis: verum

end;

defpred S₁[ Nat] means (l1 SubstWith l2) | ((S -termsOfMaxDepth) . $1) is Function of ((S -termsOfMaxDepth) . $1),((S -termsOfMaxDepth) . $1);
A3: S₁[ 0 ]

proof

reconsider z = 0 as Element of NAT ;
reconsider T0 = (S -termsOfMaxDepth) . z as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
set f = (l1 SubstWith l2) | T0;
A4: dom ((l1 SubstWith l2) | T0) = T0 by PARTFUN1:def 2;

now :: thesis: for x being object st x in T0 holds
((l1 SubstWith l2) | T0) . x in T0

let x be object ; :: thesis: ( x in T0 implies ((l1 SubstWith l2) | T0) . x in T0 )
assume A5: x in T0 ; :: thesis: ((l1 SubstWith l2) | T0) . x in T0
reconsider t = x as 0 -termal string of S by A5, FOMODEL1:def 33;
set l = (S -firstChar) . t;
reconsider tt = t as Element of T0 by FOMODEL1:def 33;
(((l1 SubstWith l2) | T0) . tt) \+\ ((l1 SubstWith l2) . tt) = {} ;
then ((l1 SubstWith l2) | T0) . x = (l1 SubstWith l2) . x by FOMODEL0:29;
then ((l1 SubstWith l2) | T0) . t in T0 by A1;
hence ((l1 SubstWith l2) | T0) . x in T0 ; :: thesis: verum

end;

hence S₁[ 0 ] by A4, FUNCT_2:3; :: thesis: verum

end;

A6: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
reconsider mm = m, MM = m + 1 as Element of NAT by ORDINAL1:def 12;
assume A7: S₁[m] ; :: thesis: S₁[m + 1]
reconsider Tm = (S -termsOfMaxDepth) . mm, TM = (S -termsOfMaxDepth) . MM as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
reconsider f = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) as Function of ((S -termsOfMaxDepth) . mm),((S -termsOfMaxDepth) . mm) by A7;
set ff = (l1 SubstWith l2) | TM;
A8: dom ((l1 SubstWith l2) | TM) = TM by PARTFUN1:def 2;

now :: thesis: for tt being object st tt in TM holds
((l1 SubstWith l2) | TM) . tt in (S -termsOfMaxDepth) . (mm + 1)

let tt be object ; :: thesis: ( tt in TM implies ((l1 SubstWith l2) | TM) . tt in (S -termsOfMaxDepth) . (mm + 1) )
assume tt in TM ; :: thesis: ((l1 SubstWith l2) | TM) . tt in (S -termsOfMaxDepth) . (mm + 1)
then reconsider ttt = tt as Element of TM ;
reconsider t = ttt as mm + 1 -termal string of S by TARSKI:def 3, FOMODEL1:def 33;
set ST = SubTerms t;
dom f = (S -termsOfMaxDepth) . mm by FUNCT_2:def 1;
then rng (SubTerms t) c= dom f by RELAT_1:def 19;
then A9: (l1 SubstWith l2) * (SubTerms t) = f * (SubTerms t) by RELAT_1:165;
reconsider s = (S -firstChar) . t as termal Element of S ;
set l = |.(ar s).|;
f * (SubTerms t) is FinSequence of (S -termsOfMaxDepth) . mm by FOMODEL0:26;
then reconsider newtt = f * (SubTerms t) as |.(ar s).| -element Element of ((S -termsOfMaxDepth) . mm) * ;
(((l1 SubstWith l2) | TM) . ttt) \+\ ((l1 SubstWith l2) . ttt) = {} ;
then A10: ((l1 SubstWith l2) | TM) . tt = (l1 SubstWith l2) . tt by FOMODEL0:29;
( ( s = l1 implies ( (l1 SubstWith l2) . <*s*> = <*l2*> & ar s = ar l2 ) ) & ( s <> l1 implies ( (l1 SubstWith l2) . <*s*> = <*s*> & ar s = ar s ) ) ) by FOMODEL0:35;
then consider ss being termal Element of S such that
A11: ( (l1 SubstWith l2) . <*s*> = <*ss*> & ar s = ar ss ) ;
reconsider newttt = newtt as |.(ar ss).| -element Element of ((S -termsOfMaxDepth) . mm) * by A11;
(l1 SubstWith l2) . t = (l1 SubstWith l2) . (<*((S -firstChar) . t)*> ^ ((S -multiCat) . (SubTerms t))) by FOMODEL1:def 37
.= ((l1 SubstWith l2) . <*s*>) ^ ((l1 SubstWith l2) . ((S -multiCat) . (SubTerms t))) by FOMODEL0:36
.= ss -compound newttt by FOMODEL0:37, A9, A11 ;
hence ((l1 SubstWith l2) | TM) . tt in (S -termsOfMaxDepth) . (mm + 1) by A10, FOMODEL1:def 33; :: thesis: verum

end;

hence S₁[m + 1] by A8, FUNCT_2:3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
hence (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) is Function of ((S -termsOfMaxDepth) . m),((S -termsOfMaxDepth) . m) ; :: thesis: verum