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 S1[ expression of C] means $1 at (C idval X) = $1;
A1: for x being variable holds S1[x -term C]
proof
let x be variable; :: thesis: S1[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 S1[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
S1[t] ) holds
S1[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
S1[t] ) holds
S1[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
S1[t] ) implies S1[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
S1[t] ; :: thesis: S1[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 S1[c -trm p] by A5, Def60; :: thesis: verum
end;
A10: for a being expression of C, an_Adj C st S1[a] holds
S1[(non_op C) term a] by Def60;
A11: 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)] by Def60;
thus S1[e] from ABCMIZ_1:sch 2(A1, A4, A10, A11); :: thesis: verum