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 let i be
set ;
( i in the carrier of IIG implies for f being Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) st f = f1 . i holds
(f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i) )assume A8:
i in the
carrier of
IIG
;
for f being Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) st f = f1 . i holds
(f2 || (FreeGen the Sorts of A)) . i = f | ((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, PBOOLE:def 2;
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;
let f be
Function of
( the Sorts of (FreeMSA the Sorts of A) . i),
( the Sorts of (FreeMSA the Sorts of A) . i);
( f = f1 . i implies (f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i) )assume
f = f1 . i
;
(f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i)then A11:
(Fix_inp iv) . i c= f
by A5, A8, PBOOLE:def 2;
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
.=
f | ((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