reconsider G = FreeGen the Sorts of A as free GeneratorSet of FreeEnv A by MSAFREE:16;
consider h being ManySortedFunction of (FreeEnv A),(FreeEnv A) such that
A1: h is_homomorphism FreeEnv A, FreeEnv A and
A2: h || G = Fix_inp iv by MSAFREE:def 5;
take h ; :: thesis: ( h is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= h )
thus h is_homomorphism FreeEnv A, FreeEnv A by A1; :: thesis: Fix_inp iv c= h
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of IIG or (Fix_inp iv) . i c= h . i )
assume A3: i in the carrier of IIG ; :: thesis: (Fix_inp iv) . i c= h . i
then reconsider hi = h . i as Function of ( the Sorts of (FreeEnv A) . i),( the Sorts of (FreeEnv A) . i) by PBOOLE:def 15;
(Fix_inp iv) . i = hi | (G . i) by A2, A3, MSAFREE:def 1;
hence (Fix_inp iv) . i c= h . i by RELAT_1:59; :: thesis: verum