reconsider d = (h . a) . t as Element of the Sorts of C . a by FUNCT_2:5;
take d ; :: thesis: ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & d = (f . a) . t )
take h ; :: thesis: ex Q being GeneratorSet of T st
( h is_homomorphism T,C & Q = doms s & s = h || Q & d = (h . a) . t )
thus ex Q being GeneratorSet of T st
( h is_homomorphism T,C & Q = doms s & s = h || Q & d = (h . a) . t ) by A1; :: thesis: verum