let h1, h2 be ManySortedFunction of (FreeEnv A),(FreeEnv A); ( 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
; h1 = h2
reconsider f1 = h1, f2 = h2 as ManySortedFunction of (FreeMSA the Sorts of A),(FreeMSA the Sorts of A) ;
now 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 ;
( 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
;
(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
;
verum end;
then
f1 || (FreeGen the Sorts of A) = f2 || (FreeGen the Sorts of A)
by MSAFREE:def 1;
hence
h1 = h2
by A4, A6, EXTENS_1:14; verum