let C be initialized ConstructorSignature; :: thesis: for e being expression of C
for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2)
let e be expression of C; :: thesis: for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2)
set t = e;
let f1, f2 be valuation of C; :: thesis: (e at f1) at f2 = e at (f1 at f2)
A0: dom (f1 at f2) = (dom f1) \/ (dom f2) by SUBST2;
defpred S₁[ expression of C] means ($1 at f1) at f2 = $1 at (f1 at f2);
W1: for x being variable holds S₁[x -term C]

proof

let x be variable; :: thesis: S₁[x -term C]

per cases ( x in dom (f1 at f2) or x nin dom (f1 at f2) ) ;

suppose Z0: x in dom (f1 at f2) ; :: thesis: S₁[x -term C]

then (x -term C) at (f1 at f2) = (f1 at f2) . x by SUBST;
hence S₁[x -term C] by Z0, SUBST2; :: thesis: verum

end;

suppose Z0: x nin dom (f1 at f2) ; :: thesis: S₁[x -term C]

then ( x nin dom f1 & x nin dom f2 ) by A0, XBOOLE_0:def 3;
then ( (x -term C) at f1 = x -term C & (x -term C) at f2 = x -term C ) by SUBST;
hence S₁[x -term C] by Z0, SUBST; :: thesis: verum

end;

end;

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]
Z5: ( len (p at f1) = len p & len (p at (f1 at f2)) = len p & len ((p at f1) at f2) = len (p at f1) ) by ThTr2;
then Z2: ( dom (p at f1) = dom p & dom (p at (f1 at f2)) = dom p & dom ((p at f1) at f2) = dom p ) by FINSEQ_3:31;

now

let i be Nat; :: thesis: ( i in dom p implies ((p at f1) at f2) . i = (p at (f1 at f2)) . i )
assume i in dom p ; :: thesis: ((p at f1) at f2) . i = (p at (f1 at f2)) . i
then Z3: ( ((p at f1) at f2) . i = (f2 # ) . ((p at f1) . i) & (p at f1) . i = (f1 # ) . (p . i) & (p at (f1 at f2)) . i = ((f1 at f2) # ) . (p . i) & p . i in rng p ) by Z2, 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;
thus ((p at f1) at f2) . i = (pi at f1) at f2 by Z3
.= pi at (f1 at f2) by Z1, Z3
.= (p at (f1 at f2)) . i by Z3 ; :: thesis: verum

end;

then Z4: (p at f1) at f2 = p at (f1 at f2) by Z2, FINSEQ_1:17;
thus ((c -trm p) at f1) at f2 = (c -trm (p at f1)) at f2 by Z0, SUBST
.= c -trm (p at (f1 at f2)) by Z0, Z5, Z4, SUBST
.= (c -trm p) at (f1 at f2) 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]

proof

let a be expression of C, an_Adj C; :: thesis: ( S₁[a] implies S₁[(non_op C) term a] )
assume S₁[a] ; :: thesis: S₁[(non_op C) term a]
then ((non_op C) term (a at f1)) at f2 = (non_op C) term (a at (f1 at f2)) by SUBST
.= ((non_op C) term a) at (f1 at f2) by SUBST ;
hence S₁[(non_op C) term a] by SUBST; :: thesis: verum

end;

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]

proof

let a be expression of C, an_Adj C; :: thesis: ( S₁[a] implies for t being expression of C, a_Type C st S₁[t] holds
S₁[(ast C) term a,t] )
assume Z1: S₁[a] ; :: thesis: for t being expression of C, a_Type C st S₁[t] holds
S₁[(ast C) term a,t]
let t be expression of C, a_Type C; :: thesis: ( S₁[t] implies S₁[(ast C) term a,t] )
assume S₁[t] ; :: thesis: S₁[(ast C) term a,t]
then ((ast C) term (a at f1),(t at f1)) at f2 = (ast C) term (a at (f1 at f2)),(t at (f1 at f2)) by Z1, SUBST
.= ((ast C) term a,t) at (f1 at f2) by SUBST ;
hence S₁[(ast C) term a,t] by SUBST; :: thesis: verum

end;

thus S₁[e] from ABCMIZ_1:sch 2(W1, W2, W3, W4); :: thesis: verum