let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds
(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds
(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds
(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2
set H = canonical_homomorphism T;
let t1, t2 be Element of (Free (S,X)); :: thesis: ( t2 = (canonical_homomorphism T) . t1 implies (canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2 )
assume Z0: t2 = (canonical_homomorphism T) . t1 ; :: thesis: (canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2
reconsider t = t1 as Element of the Sorts of (Free (S,X)) . (the_sort_of t1) by SORT;
A1: ( the_sort_of (@ ((canonical_homomorphism T) . t1)) = the_sort_of ((canonical_homomorphism T) . t1) & (canonical_homomorphism T) . (the_sort_of t1) is Function of ( the Sorts of (Free (S,X)) . (the_sort_of t1)),( the Sorts of T . (the_sort_of t1)) ) by Lem00;
A2: ( dom ((canonical_homomorphism T) ** (canonical_homomorphism T)) = (dom (canonical_homomorphism T)) /\ (dom (canonical_homomorphism T)) & (dom (canonical_homomorphism T)) /\ (dom (canonical_homomorphism T)) = dom (canonical_homomorphism T) & dom (canonical_homomorphism T) = the carrier of S ) by PARTFUN1:def 2, PBOOLE:def 19;
(canonical_homomorphism T) ** (canonical_homomorphism T) = canonical_homomorphism T by MSAFREE4:48;
hence (canonical_homomorphism T) . t1 = (((canonical_homomorphism T) ** (canonical_homomorphism T)) . (the_sort_of t1)) . t1 by ABBR
.= (((canonical_homomorphism T) . (the_sort_of t1)) * ((canonical_homomorphism T) . (the_sort_of t1))) . t by A2, PBOOLE:def 19
.= ((canonical_homomorphism T) . (the_sort_of t1)) . (((canonical_homomorphism T) . (the_sort_of t1)) . t1) by FUNCT_2:15
.= ((canonical_homomorphism T) . (the_sort_of t1)) . ((canonical_homomorphism T) . t1) by ABBR
.= ((canonical_homomorphism T) . (the_sort_of t2)) . ((canonical_homomorphism T) . t1) by Z0, A1, Lem0
.= (canonical_homomorphism T) . t2 by Z0, ABBR ;
:: thesis: verum