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

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