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) ex g being Endomorphism of T st
( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ 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) ex g being Endomorphism of T st
( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ 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) ex g being Endomorphism of T st
( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )
let h be Endomorphism of Free (S,X); :: thesis: ex g being Endomorphism of T st
( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )
set H = canonical_homomorphism T;
( canonical_homomorphism T is_homomorphism Free (S,X),T & h is_homomorphism Free (S,X), Free (S,X) ) by MSUALG_6:def 2, MSAFREE4:def 10;
then consider g being ManySortedFunction of T,T such that
A1: ( g is_homomorphism T,T & (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) ) by MSAFREE4:65, MSUALG_3:10;
reconsider g = g as Endomorphism of T by A1, MSUALG_6:def 2;
take g ; :: thesis: ( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )
thus (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) by A1; :: thesis: for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t))
let t be Element of T; :: thesis: g . t = (canonical_homomorphism T) . (h . (@ t))
thus g . t = g . ((canonical_homomorphism T) . (@ t))
.= (g ** (canonical_homomorphism T)) . (@ t) by Th14
.= (canonical_homomorphism T) . (h . (@ t)) by A1, Th14 ; :: thesis: verum