let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A being b1,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 V5() ManySortedSet of S; 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; 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; 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); 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))); ( x0 = x implies (canonical_homomorphism A) # x0 = x )
assume A1:
x0 = x
; (canonical_homomorphism A) # x0 = x
set k = canonical_homomorphism A;
now 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;
( n in dom x0 implies x . n = ((canonical_homomorphism A) . ((the_arity_of o) /. n)) . (x0 . n) )assume A2:
n in dom x0
;
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;
verum end;
hence
(canonical_homomorphism A) # x0 = x
by MSUALG_3:def 6; verum