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

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