let h1, h2 be ManySortedFunction of (FreeEnv A),(FreeEnv A); :: thesis: ( h1 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= h1 & h2 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= h2 implies h1 = h2 )

assume that

A4: h1 is_homomorphism FreeEnv A, FreeEnv A and

A5: Fix_inp iv c= h1 and

A6: h2 is_homomorphism FreeEnv A, FreeEnv A and

A7: Fix_inp iv c= h2 ; :: thesis: h1 = h2

reconsider f1 = h1, f2 = h2 as ManySortedFunction of (FreeMSA the Sorts of A),(FreeMSA the Sorts of A) ;

hence h1 = h2 by A4, A6, EXTENS_1:14; :: thesis: verum

assume that

A4: h1 is_homomorphism FreeEnv A, FreeEnv A and

A5: Fix_inp iv c= h1 and

A6: h2 is_homomorphism FreeEnv A, FreeEnv A and

A7: Fix_inp iv c= h2 ; :: thesis: h1 = h2

reconsider f1 = h1, f2 = h2 as ManySortedFunction of (FreeMSA the Sorts of A),(FreeMSA the Sorts of A) ;

now :: thesis: for i being set st i in the carrier of IIG holds

(f2 || (FreeGen the Sorts of A)) . i = (f1 . i) | ((FreeGen the Sorts of A) . i)

then
f1 || (FreeGen the Sorts of A) = f2 || (FreeGen the Sorts of A)
by MSAFREE:def 1;(f2 || (FreeGen the Sorts of A)) . i = (f1 . i) | ((FreeGen the Sorts of A) . i)

let i be set ; :: thesis: ( i in the carrier of IIG implies (f2 || (FreeGen the Sorts of A)) . i = (f1 . i) | ((FreeGen the Sorts of A) . i) )

assume A8: i in the carrier of IIG ; :: thesis: (f2 || (FreeGen the Sorts of A)) . i = (f1 . i) | ((FreeGen the Sorts of A) . i)

reconsider g = f2 . i as Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) by A8, PBOOLE:def 15;

A9: (Fix_inp iv) . i c= g by A7, A8;

reconsider Fi = (Fix_inp iv) . i as Function ;

Fi is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) by A8, PBOOLE:def 15;

then A10: dom Fi = (FreeGen the Sorts of A) . i by A8, FUNCT_2:def 1;

A11: (Fix_inp iv) . i c= f1 . i by A5, A8;

thus (f2 || (FreeGen the Sorts of A)) . i = g | ((FreeGen the Sorts of A) . i) by A8, MSAFREE:def 1

.= (Fix_inp iv) . i by A10, A9, GRFUNC_1:23

.= (f1 . i) | ((FreeGen the Sorts of A) . i) by A10, A11, GRFUNC_1:23 ; :: thesis: verum

end;assume A8: i in the carrier of IIG ; :: thesis: (f2 || (FreeGen the Sorts of A)) . i = (f1 . i) | ((FreeGen the Sorts of A) . i)

reconsider g = f2 . i as Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) by A8, PBOOLE:def 15;

A9: (Fix_inp iv) . i c= g by A7, A8;

reconsider Fi = (Fix_inp iv) . i as Function ;

Fi is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) by A8, PBOOLE:def 15;

then A10: dom Fi = (FreeGen the Sorts of A) . i by A8, FUNCT_2:def 1;

A11: (Fix_inp iv) . i c= f1 . i by A5, A8;

thus (f2 || (FreeGen the Sorts of A)) . i = g | ((FreeGen the Sorts of A) . i) by A8, MSAFREE:def 1

.= (Fix_inp iv) . i by A10, A9, GRFUNC_1:23

.= (f1 . i) | ((FreeGen the Sorts of A) . i) by A10, A11, GRFUNC_1:23 ; :: thesis: verum

hence h1 = h2 by A4, A6, EXTENS_1:14; :: thesis: verum