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 S1[ expression of C] means ($1 at f1) at f2 = $1 at (f1 at f2);
A2: for x being variable holds S1[x -term C]
proof
let x be variable; :: thesis: S1[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: S1[x -term C]
then (x -term C) at (f1 at f2) = (f1 at f2) . x by Def60;
hence S1[x -term C] by A3, Def66; :: 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
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
A9: len p = len (the_arity_of c) and
A10: for t being quasi-term of C st t in rng p holds
S1[t] ; :: thesis: S1[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 S1[a] holds
S1[(non_op C) term a]
proof
let a be expression of C, an_Adj C; :: thesis: ( S1[a] implies S1[(non_op C) term a] )
assume S1[a] ; :: thesis: S1[(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 S1[(non_op C) term a] by Def60; :: thesis: verum
end;
A22: 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)]
proof
let a be expression of C, an_Adj C; :: thesis: ( S1[a] implies for t being expression of C, a_Type C st S1[t] holds
S1[(ast C) term (a,t)] )
assume A23: S1[a] ; :: thesis: for t being expression of C, a_Type C st S1[t] holds
S1[(ast C) term (a,t)]
let t be expression of C, a_Type C; :: thesis: ( S1[t] implies S1[(ast C) term (a,t)] )
assume S1[t] ; :: thesis: S1[(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 S1[(ast C) term (a,t)] by Def60; :: thesis: verum
end;
thus S1[e] from ABCMIZ_1:sch 2(A2, A8, A21, A22); :: thesis: verum