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)
A1: dom (f1 at f2) = (dom f1) \/ (dom f2) by Def66;
defpred S₁[ expression of C] means ($1 at f1) at f2 = $1 at (f1 at f2);
A2: 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 A3: x in dom (f1 at f2) ; :: thesis: S₁[x -term C]

then (x -term C) at (f1 at f2) = (f1 at f2) . x by Def60;
hence S₁[x -term C] by A3, Def66; :: thesis: verum

end;

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

then A5: x nin dom f1 by A1, XBOOLE_0:def 3;
A6: x nin dom f2 by A1, A4, XBOOLE_0:def 3;
A7: (x -term C) at f1 = x -term C by A5, Def60;
(x -term C) at f2 = x -term C by A6, Def60;
hence S₁[x -term C] by A4, A7, Def60; :: thesis: verum

end;

end;

end;

A8: 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
A9: len p = len (the_arity_of c) and
A10: for t being quasi-term of C st t in rng p holds
S₁[t] ; :: thesis: S₁[c -trm p]
A11: len (p at f1) = len p by Th130;
A12: len (p at (f1 at f2)) = len p by Th130;
A13: len ((p at f1) at f2) = len (p at f1) by Th130;
A14: dom (p at f1) = dom p by A11, FINSEQ_3:29;
A15: dom (p at (f1 at f2)) = dom p by A12, FINSEQ_3:29;
A16: dom ((p at f1) at f2) = dom p by A11, A13, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom p holds
((p at f1) at f2) . i = (p at (f1 at f2)) . i

let i be Nat; :: thesis: ( i in dom p implies ((p at f1) at f2) . i = (p at (f1 at f2)) . i )
assume A17: i in dom p ; :: thesis: ((p at f1) at f2) . i = (p at (f1 at f2)) . i
then A18: ((p at f1) at f2) . i = (f2 #) . ((p at f1) . i) by A14, FUNCT_1:13;
A19: p . i in rng p by A17, 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 A19, Th41;
thus ((p at f1) at f2) . i = (pi1 at f1) at f2 by A17, A18, FUNCT_1:13
.= pi1 at (f1 at f2) by A10, A19
.= (p at (f1 at f2)) . i by A17, FUNCT_1:13 ; :: thesis: verum

end;

then A20: (p at f1) at f2 = p at (f1 at f2) by A15, A16;
thus ((c -trm p) at f1) at f2 = (c -trm (p at f1)) at f2 by A9, Def60
.= c -trm (p at (f1 at f2)) by A9, A11, A20, Def60
.= (c -trm p) at (f1 at f2) by A9, Def60 ; :: thesis: verum

end;

A21: 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 Def60
.= ((non_op C) term a) at (f1 at f2) by Def60 ;
hence S₁[(non_op C) term a] by Def60; :: thesis: verum

end;

A22: 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 A23: 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 A23, Def60
.= ((ast C) term (a,t)) at (f1 at f2) by Def60 ;
hence S₁[(ast C) term (a,t)] by Def60; :: thesis: verum

end;

thus S₁[e] from ABCMIZ_1:sch 2(A2, A8, A21, A22); :: thesis: verum