let C be initialized ConstructorSignature; :: thesis: for e being expression of C
for X being Subset of Vars holds e at (C idval X) = e
let e be expression of C; :: thesis: for X being Subset of Vars holds e at (C idval X) = e
set t = e;
let X be Subset of Vars ; :: thesis: e at (C idval X) = e
set f = C idval X;
defpred S₁[ expression of C] means $1 at (C idval X) = $1;
W1: for x being variable holds S₁[x -term C]

proof

let x be variable; :: thesis: S₁[x -term C]
( ( x in X or x nin X ) & dom (C idval X) = X & ( x in X implies (C idval X) . x = x -term C ) ) by ThIV;
hence S₁[x -term C] by SUBST; :: thesis: verum

end;

W2: 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
S₁[t] ) holds
S₁[c -trm p]

proof

let c be constructor OperSymbol of C; :: thesis: 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
S₁[t] ) holds
S₁[c -trm p]
let p be FinSequence of QuasiTerms C; :: thesis: ( len p = len (the_arity_of c) & ( for t being quasi-term of C st t in rng p holds
S₁[t] ) implies S₁[c -trm p] )
assume that
Z0: len p = len (the_arity_of c) and
Z1: for t being quasi-term of C st t in rng p holds
S₁[t] ; :: thesis: S₁[c -trm p]
len (p at (C idval X)) = len p by ThTr2;
then Z2: dom (p at (C idval X)) = dom p by FINSEQ_3:31;

now

let i be Nat; :: thesis: ( i in dom p implies (p at (C idval X)) . i = p . i )
assume i in dom p ; :: thesis: (p at (C idval X)) . i = p . i
then Z3: ( (p at (C idval X)) . i = ((C idval X) # ) . (p . i) & p . i in rng p ) by FUNCT_1:23, FUNCT_1:def 5;
rng p c= QuasiTerms C by FINSEQ_1:def 4;
then reconsider pi = p . i as quasi-term of C by Z3, Th42;
(p at (C idval X)) . i = pi at (C idval X) by Z3;
hence (p at (C idval X)) . i = p . i by Z1, Z3; :: thesis: verum

end;

then p at (C idval X) = p by Z2, FINSEQ_1:17;
hence S₁[c -trm p] by Z0, SUBST; :: thesis: verum

end;

W3: for a being expression of C, an_Adj C st S₁[a] holds
S₁[(non_op C) term a] by SUBST;
W4: for a being expression of C, an_Adj C st S₁[a] holds
for t being expression of C, a_Type C st S₁[t] holds
S₁[(ast C) term a,t] by SUBST;
thus S₁[e] from ABCMIZ_1:sch 2(W1, W2, W3, W4); :: thesis: verum