let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let x be Element of X . s; :: thesis: for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let t be Element of (Free (S,X)); :: thesis: for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let C be context of x; :: thesis: ( X is non-trivial implies for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t) )
assume ZZ: X is non-trivial ; :: thesis: for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)
let xi be Element of dom C; :: thesis: ( C . xi = [x,s] & the_sort_of t = s implies C -sub t = C with-replacement (xi,t) )
assume Z0: C . xi = [x,s] ; :: thesis: ( not the_sort_of t = s or C -sub t = C with-replacement (xi,t) )
assume Z1: the_sort_of t = s ; :: thesis: C -sub t = C with-replacement (xi,t)
defpred S₁[ Element of (Free (S,X))] means for C being context of x st C = $1 holds
for xi being Element of dom C st C . xi = [x,s] holds
C -sub t = C with-replacement (xi,t);
A1: S₁[x -term ]

proof

let C be context of x; :: thesis: ( C = x -term implies for xi being Element of dom C st C . xi = [x,s] holds
C -sub t = C with-replacement (xi,t) )
assume A2: C = x -term ; :: thesis: for xi being Element of dom C st C . xi = [x,s] holds
C -sub t = C with-replacement (xi,t)
let xi be Element of dom C; :: thesis: ( C . xi = [x,s] implies C -sub t = C with-replacement (xi,t) )
xi in {{}} by A2, TREES_1:29;
then xi = <*> NAT ;
hence ( C . xi = [x,s] implies C -sub t = C with-replacement (xi,t) ) by Z1, A2, Th41; :: thesis: verum

end;

A3: for o being OperSymbol of S
for w being Element of Args (o,(Free (S,X))) st w is x -context_including & S₁[x -context_in w] holds
for C being context of x st C = o -term w holds
S₁[C]

proof

let o be OperSymbol of S; :: thesis: for w being Element of Args (o,(Free (S,X))) st w is x -context_including & S₁[x -context_in w] holds
for C being context of x st C = o -term w holds
S₁[C]
let w be Element of Args (o,(Free (S,X))); :: thesis: ( w is x -context_including & S₁[x -context_in w] implies for C being context of x st C = o -term w holds
S₁[C] )
assume Z2: w is x -context_including ; :: thesis: ( not S₁[x -context_in w] or for C being context of x st C = o -term w holds
S₁[C] )
assume Z3: S₁[x -context_in w] ; :: thesis: for C being context of x st C = o -term w holds
S₁[C]
let C be context of x; :: thesis: ( C = o -term w implies S₁[C] )
assume Z4: C = o -term w ; :: thesis: S₁[C]
let D be context of x; :: thesis: ( D = C implies for xi being Element of dom D st D . xi = [x,s] holds
D -sub t = D with-replacement (xi,t) )
assume Z5: D = C ; :: thesis: for xi being Element of dom D st D . xi = [x,s] holds
D -sub t = D with-replacement (xi,t)
let xi be Element of dom D; :: thesis: ( D . xi = [x,s] implies D -sub t = D with-replacement (xi,t) )
assume Z6: D . xi = [x,s] ; :: thesis: D -sub t = D with-replacement (xi,t)
dom D = tree (doms w) by Z4, Z5, TREES_4:10;

per cases then ( xi = {} or ex i being Nat ex r being FinSequence st
( i < len (doms w) & r in (doms w) . (i + 1) & xi = <*i*> ^ r ) ) by TREES_3:def 15;

suppose xi = {} ; :: thesis: D -sub t = D with-replacement (xi,t)

then D . xi = [o, the carrier of S] by Z4, Z5, TREES_4:def 4;
then ( s in the carrier of S & the carrier of S = s ) by Z6, XTUPLE_0:1;
hence D -sub t = D with-replacement (xi,t) ; :: thesis: verum

end;

suppose ex i being Nat ex r being FinSequence st
( i < len (doms w) & r in (doms w) . (i + 1) & xi = <*i*> ^ r ) ; :: thesis: D -sub t = D with-replacement (xi,t)

then consider i being Nat, r being FinSequence such that
A4: ( i < len (doms w) & r in (doms w) . (i + 1) & xi = <*i*> ^ r ) ;
A5: len (doms w) = len w by TREES_3:38;
then AB: ( 1 <= i + 1 & i + 1 <= len w ) by A4, NAT_1:12, NAT_1:13;
then A6: i + 1 in dom w by FINSEQ_3:25;
then A7: ( w /. (i + 1) = w . (i + 1) & w . (i + 1) in rng w & (doms w) . (i + 1) = dom (w . (i + 1)) ) by PARTFUN1:def 6, FUNCT_6:def 2, FUNCT_1:def 3;
then reconsider r = r as Element of dom (w /. (i + 1)) by A4;
A8: ( D . xi = (w /. (i + 1)) . r & [x,s] in {[x,s]} ) by Z4, Z5, A4, A5, A7, TARSKI:def 1, TREES_4:12;
then not w /. (i + 1) is x -omitting by Z6, FUNCT_1:def 7;
then AA: x -context_pos_in w = i + 1 by Z2, AB, Th72, FINSEQ_3:25;
then A9: x -context_in w = w /. (i + 1) by Z2, A7, Th71;
the_sort_of (x -context_in w) = (the_arity_of o) /. (x -context_pos_in w) by A6, AA, A9, Th4A;
then reconsider u = w +* ((x -context_pos_in w),((x -context_in w) -sub t)) as Element of Args (o,(Free (S,X))) by MSUALG_6:7;
A11: D -sub t = o -term u by ZZ, Z1, Z2, Z4, Z5, Th43;
xi in dom D ;
then ( i < len w & xi in tree (doms w) & x -context_in w = w . (i + 1) & u = w +* ((i + 1),((x -context_in w) with-replacement (r,t))) ) by Z4, Z5, A4, AA, A9, Z3, Z6, A8, A6, TREES_3:38, TREES_4:10, PARTFUN1:def 6;
hence D -sub t = D with-replacement (xi,t) by A11, Z4, Z5, A4, Th123; :: thesis: verum

end;

end;

end;

S₁[C] from MSAFREE5:sch 4(A1, A3);
hence C -sub t = C with-replacement (xi,t) by Z0; :: thesis: verum