let C be initialized ConstructorSignature; for f, g being one-to-one irrelevant valuation of C st ( for x, y being variable st x in dom f & f . x = y -term C holds
( y in dom g & g . y = x -term C ) ) holds
for e being expression of C st variables_in e c= dom f holds
(e at f) at g = e
let f, g be one-to-one irrelevant valuation of C; ( ( for x, y being variable st x in dom f & f . x = y -term C holds
( y in dom g & g . y = x -term C ) ) implies for e being expression of C st variables_in e c= dom f holds
(e at f) at g = e )
assume A1:
for x, y being variable st x in dom f & f . x = y -term C holds
( y in dom g & g . y = x -term C )
; for e being expression of C st variables_in e c= dom f holds
(e at f) at g = e
let t be expression of C; ( variables_in t c= dom f implies (t at f) at g = t )
defpred S1[ expression of C] means ( variables_in $1 c= dom f implies ($1 at f) at g = $1 );
A2:
for x being variable holds S1[x -term C]
A7:
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & ( for t being quasi-term of C st t in rng p holds
S1[t] ) holds
S1[c -trm p]
proof
let c be
constructor OperSymbol of
C;
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & ( for t being quasi-term of C st t in rng p holds
S1[t] ) holds
S1[c -trm p]let p be
FinSequence of
QuasiTerms C;
( len p = len (the_arity_of c) & ( for t being quasi-term of C st t in rng p holds
S1[t] ) implies S1[c -trm p] )
assume that A8:
len p = len (the_arity_of c)
and A9:
for
t being
quasi-term of
C st
t in rng p holds
S1[
t]
and A10:
variables_in (c -trm p) c= dom f
;
((c -trm p) at f) at g = c -trm p
c -trm p = [c, the carrier of C] -tree p
by A8, Def35;
then A11:
variables_in (c -trm p) = union { (variables_in s) where s is quasi-term of C : s in rng p }
by Th88;
A12:
len (p at f) = len p
by Th130;
A13:
len ((p at f) at g) = len (p at f)
by Th130;
A14:
dom (p at f) = dom p
by A12, FINSEQ_3:29;
A15:
dom ((p at f) at g) = dom (p at f)
by A13, FINSEQ_3:29;
now for i being Nat st i in dom p holds
((p at f) at g) . i = p . ilet i be
Nat;
( i in dom p implies ((p at f) at g) . i = p . i )assume A16:
i in dom p
;
((p at f) at g) . i = p . ithen A17:
(p at f) . i = (f #) . (p . i)
by FUNCT_1:13;
A18:
p . i in rng p
by A16, FUNCT_1:def 3;
rng p c= QuasiTerms C
by FINSEQ_1:def 4;
then reconsider pi1 =
p . i as
quasi-term of
C by A18, Th41;
variables_in pi1 in { (variables_in s) where s is quasi-term of C : s in rng p }
by A18;
then A19:
variables_in pi1 c= variables_in (c -trm p)
by A11, ZFMISC_1:74;
((p at f) at g) . i = (pi1 at f) at g
by A14, A16, A17, FUNCT_1:13;
hence
((p at f) at g) . i = p . i
by A9, A10, A18, A19, XBOOLE_1:1;
verum end;
then A20:
(p at f) at g = p
by A14, A15;
(c -trm p) at f = c -trm (p at f)
by A8, Def60;
hence
((c -trm p) at f) at g = c -trm p
by A8, A12, A20, Def60;
verum
end;
A21:
for a being expression of C, an_Adj C st S1[a] holds
S1[(non_op C) term a]
A25:
for a being expression of C, an_Adj C st S1[a] holds
for t being expression of C, a_Type C st S1[t] holds
S1[(ast C) term (a,t)]
proof
let a be
expression of
C,
an_Adj C;
( S1[a] implies for t being expression of C, a_Type C st S1[t] holds
S1[(ast C) term (a,t)] )
assume A26:
S1[
a]
;
for t being expression of C, a_Type C st S1[t] holds
S1[(ast C) term (a,t)]
let t be
expression of
C,
a_Type C;
( S1[t] implies S1[(ast C) term (a,t)] )
assume that A27:
S1[
t]
and A28:
variables_in ((ast C) term (a,t)) c= dom f
;
(((ast C) term (a,t)) at f) at g = (ast C) term (a,t)
(ast C) term (
a,
t)
= [*, the carrier of C] -tree <*a,t*>
by Th46;
then A29:
variables_in ((ast C) term (a,t)) =
((C variables_in a) (\/) (C variables_in t)) . a_Term
by Th96
.=
(variables_in a) \/ (variables_in t)
by PBOOLE:def 4
;
thus (((ast C) term (a,t)) at f) at g =
((ast C) term ((a at f),(t at f))) at g
by Def60
.=
(ast C) term (
a,
t)
by A26, A27, A28, A29, Def60, XBOOLE_1:11
;
verum
end;
thus
S1[t]
from ABCMIZ_1:sch 2(A2, A7, A21, A25); verum