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

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

let n be Nat; :: thesis: ( n in dom x0 implies x . n = ((canonical_homomorphism A) . ((the_arity_of o) /. n)) . (x0 . n) )
assume A2: n in dom x0 ; :: thesis: x . n = ((canonical_homomorphism A) . ((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 A * (the_arity_of o)) = dom x by A3, PRALG_2:3;
then x . n in ( the Sorts of A * (the_arity_of o)) . n by A1, A2, MSUALG_3:6;
then x . n is Element of A,((the_arity_of o) /. n) by A4, A2, A1, A3, FUNCT_1:13;
hence x . n = ((canonical_homomorphism A) . ((the_arity_of o) /. n)) . (x0 . n) by A1, Th47; :: thesis: verum

end;

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