let f1, f2 be term-transformation of C, MSVars C; :: thesis: ( ( for x being variable holds
( ( x in dom f implies f1 . (x -term C) = f . x ) & ( not x in dom f implies f1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f1 * p holds
f1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f1 . ((non_op C) term a) = (non_op C) term (f1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f1 . ((ast C) term (a,t)) = (ast C) term ((f1 . a),(f1 . t)) ) & ( for x being variable holds
( ( x in dom f implies f2 . (x -term C) = f . x ) & ( not x in dom f implies f2 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f2 * p holds
f2 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f2 . ((non_op C) term a) = (non_op C) term (f2 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f2 . ((ast C) term (a,t)) = (ast C) term ((f2 . a),(f2 . t)) ) implies f1 = f2 )
assume that
A7: for x being variable holds
( ( x in dom f implies f1 . (x -term C) = f . x ) & ( not x in dom f implies f1 . (x -term C) = x -term C ) ) and
A8: for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f1 * p holds
f1 . (c -trm p) = c -trm q and
A9: for a being expression of C, an_Adj C holds f1 . ((non_op C) term a) = (non_op C) term (f1 . a) and
A10: for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f1 . ((ast C) term (a,t)) = (ast C) term ((f1 . a),(f1 . t)) and
A11: for x being variable holds
( ( x in dom f implies f2 . (x -term C) = f . x ) & ( not x in dom f implies f2 . (x -term C) = x -term C ) ) and
A12: for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f2 * p holds
f2 . (c -trm p) = c -trm q and
A13: for a being expression of C, an_Adj C holds f2 . ((non_op C) term a) = (non_op C) term (f2 . a) and
A14: for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f2 . ((ast C) term (a,t)) = (ast C) term ((f2 . a),(f2 . t)) ; :: thesis: f1 = f2
set D = Union the Sorts of (Free (C,(MSVars C)));
A15: dom f1 = Union the Sorts of (Free (C,(MSVars C))) by FUNCT_2:def 1;
A16: dom f2 = Union the Sorts of (Free (C,(MSVars C))) by FUNCT_2:def 1;
defpred S₁[ expression of C] means f1 . $1 = f2 . $1;
A17: for x being variable holds S₁[x -term C]

proof

let x be variable; :: thesis: S₁[x -term C]
( ( x in dom f & f1 . (x -term C) = f . x ) or ( x nin dom f & f1 . (x -term C) = x -term C ) ) by A7;
hence S₁[x -term C] by A11; :: thesis: verum

end;

A18: 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
A19: len p = len (the_arity_of c) and
A20: for t being quasi-term of C st t in rng p holds
S₁[t] ; :: thesis: S₁[c -trm p]
A21: rng p c= QuasiTerms C by FINSEQ_1:def 4;
A22: rng (f1 * p) = f1 .: (rng p) by RELAT_1:127;
A23: rng (f2 * p) = f2 .: (rng p) by RELAT_1:127;
A24: rng (f1 * p) c= f1 .: (QuasiTerms C) by A21, A22, RELAT_1:123;
A25: rng (f2 * p) c= f2 .: (QuasiTerms C) by A21, A23, RELAT_1:123;
A26: f1 .: (QuasiTerms C) c= QuasiTerms C by Def56;
A27: f2 .: (QuasiTerms C) c= QuasiTerms C by Def56;
A28: rng (f1 * p) c= QuasiTerms C by A24, A26;
rng (f2 * p) c= QuasiTerms C by A25, A27;
then reconsider q1 = f1 * p, q2 = f2 * p as FinSequence of QuasiTerms C by A28, FINSEQ_1:def 4;
A29: rng p c= Union the Sorts of (Free (C,(MSVars C))) ;
then A30: dom q1 = dom p by A15, RELAT_1:27;
A31: dom q2 = dom p by A16, A29, RELAT_1:27;

now :: thesis: for i being Nat st i in dom p holds
q1 . i = q2 . i

let i be Nat; :: thesis: ( i in dom p implies q1 . i = q2 . i )
assume A32: i in dom p ; :: thesis: q1 . i = q2 . i
then A33: q1 . i = f1 . (p . i) by FUNCT_1:13;
A34: q2 . i = f2 . (p . i) by A32, FUNCT_1:13;
A35: p . i in rng p by A32, FUNCT_1:def 3;
then p . i is quasi-term of C by A21, Th41;
hence q1 . i = q2 . i by A20, A33, A34, A35; :: thesis: verum

end;

then f1 . (c -trm p) = c -trm q2 by A8, A19, A30, A31, FINSEQ_1:13;
hence S₁[c -trm p] by A12, A19; :: thesis: verum

end;

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

end;

A37: 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 A38: 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 f1 . ((ast C) term (a,t)) = (ast C) term ((f2 . a),(f2 . t)) by A10, A38;
hence S₁[(ast C) term (a,t)] by A14; :: thesis: verum

end;

now :: thesis: for t being expression of C holds S₁[t]

let t be expression of C; :: thesis: S₁[t]
thus S₁[t] from ABCMIZ_1:sch 2(A17, A18, A36, A37); :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum