let h1, h2 be ManySortedFunction of (),(); :: 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) ;
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)
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 ;
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 ;
then A10: dom Fi = (FreeGen the Sorts of A) . i by ;
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
.= (Fix_inp iv) . i by
.= (f1 . i) | ((FreeGen the Sorts of A) . i) by ; :: thesis: verum
end;
then f1 || (FreeGen the Sorts of A) = f2 || (FreeGen the Sorts of A) by MSAFREE:def 1;
hence h1 = h2 by ; :: thesis: verum