let S be non empty non void ManySortedSign ; :: thesis: for X0 being V5() countable ManySortedSet of S
for A0 being b₁,S -terms MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A0)
for x0 being Element of Args (o,(Free (S,X0))) st x0 = x holds
(canonical_homomorphism A0) # x0 = x
let X0 be V5() countable ManySortedSet of S; :: thesis: for A0 being X0,S -terms MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A0)
for x0 being Element of Args (o,(Free (S,X0))) st x0 = x holds
(canonical_homomorphism A0) # x0 = x
let A0 be X0,S -terms MSAlgebra over S; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,A0)
for x0 being Element of Args (o,(Free (S,X0))) st x0 = x holds
(canonical_homomorphism A0) # x0 = x
set A = A0;
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,A0)
for x0 being Element of Args (o,(Free (S,X0))) st x0 = x holds
(canonical_homomorphism A0) # x0 = x
let x be Element of Args (o,A0); :: thesis: for x0 being Element of Args (o,(Free (S,X0))) st x0 = x holds
(canonical_homomorphism A0) # x0 = x
let x0 be Element of Args (o,(Free (S,X0))); :: thesis: ( x0 = x implies (canonical_homomorphism A0) # x0 = x )
assume A1: x0 = x ; :: thesis: (canonical_homomorphism A0) # x0 = x
set k = canonical_homomorphism A0;

now :: thesis: for n being Nat st n in dom x0 holds
x . n = ((canonical_homomorphism A0) . ((the_arity_of o) /. n)) . (x0 . n)

let n be Nat; :: thesis: ( n in dom x0 implies x . n = ((canonical_homomorphism A0) . ((the_arity_of o) /. n)) . (x0 . n) )
assume A2: n in dom x0 ; :: thesis: x . n = ((canonical_homomorphism A0) . ((the_arity_of o) /. n)) . (x0 . n)
A3: dom x = dom (the_arity_of o) by MSUALG_3:6;
then A4: (the_arity_of o) /. n = (the_arity_of o) . n by A1, A2, PARTFUN1:def 6;
dom ( the Sorts of A0 * (the_arity_of o)) = dom x by A3, PRALG_2:3;
then x . n in ( the Sorts of A0 * (the_arity_of o)) . n by A1, A2, MSUALG_3:6;
then x . n is Element of A0,((the_arity_of o) /. n) by A4, A2, A1, A3, FUNCT_1:13;
hence x . n = ((canonical_homomorphism A0) . ((the_arity_of o) /. n)) . (x0 . n) by A1, Th46; :: thesis: verum

end;

hence (canonical_homomorphism A0) # x0 = x by MSUALG_3:def 6; :: thesis: verum