let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))
let X be V5() 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 h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))
let h be Endomorphism of Free (S,X); :: thesis: for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))
let t be Element of (Free (S,X)); :: thesis: (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))
set H = canonical_homomorphism T;
consider g being Endomorphism of T such that
A1: ( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) ) by Th86;
thus (canonical_homomorphism T) . (h . t) = ((canonical_homomorphism T) ** h) . t by Th14
.= g . ((canonical_homomorphism T) . t) by A1, Th14
.= (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t))) by A1 ; :: thesis: verum