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;
A1: for x being variable holds S₁[x -term C]

proof

let x be variable; :: thesis: S₁[x -term C]
A2: ( x in X or x nin X ) ;
A3: dom (C idval X) = X by Th131;
( x in X implies (C idval X) . x = x -term C ) by Th131;
hence S₁[x -term C] by A2, A3, Def60; :: thesis: verum

end;

A4: 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
A5: len p = len (the_arity_of c) and
A6: 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 Th130;
then A7: dom (p at (C idval X)) = dom p by FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom p holds
(p at (C idval X)) . i = p . i

let i be Nat; :: thesis: ( i in dom p implies (p at (C idval X)) . i = p . i )
assume A8: i in dom p ; :: thesis: (p at (C idval X)) . i = p . i
then A9: p . i in rng p by 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 A9, Th41;
(p at (C idval X)) . i = pi1 at (C idval X) by A8, FUNCT_1:13;
hence (p at (C idval X)) . i = p . i by A6, A9; :: thesis: verum

end;

then p at (C idval X) = p by A7;
hence S₁[c -trm p] by A5, Def60; :: thesis: verum

end;

A10: for a being expression of C, an_Adj C st S₁[a] holds
S₁[(non_op C) term a] by Def60;
A11: 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 Def60;
thus S₁[e] from ABCMIZ_1:sch 2(A1, A4, A10, A11); :: thesis: verum