let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds canonical_homomorphism T is x -constant
let s be SortSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds canonical_homomorphism T is x -constant
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds canonical_homomorphism T is x -constant
let x be Element of X . s; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds canonical_homomorphism T is x -constant
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: canonical_homomorphism T is x -constant
set H = canonical_homomorphism T;
thus (canonical_homomorphism T) . (x -term) = x -term ; :: according to MSAFREE5:def 29 :: thesis: for s1 being SortSymbol of S
for x1 being Element of X . s1 st ( x1 <> x or s <> s1 ) holds
(canonical_homomorphism T) . (x1 -term) is x -omitting
let s1 be SortSymbol of S; :: thesis: for x1 being Element of X . s1 st ( x1 <> x or s <> s1 ) holds
(canonical_homomorphism T) . (x1 -term) is x -omitting
let x1 be Element of X . s1; :: thesis: ( ( x1 <> x or s <> s1 ) implies (canonical_homomorphism T) . (x1 -term) is x -omitting )
assume ( x1 <> x or s <> s1 ) ; :: thesis: (canonical_homomorphism T) . (x1 -term) is x -omitting
then x1 -term is x -omitting by ThC1;
hence (canonical_homomorphism T) . (x1 -term) is x -omitting ; :: thesis: verum