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) ;
now let i be
set ;
:: thesis: ( 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
;
:: thesis: 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)let f be
Function of
(the Sorts of (FreeMSA the Sorts of A) . i),
(the Sorts of (FreeMSA the Sorts of A) . i);
:: thesis: ( f = f1 . i implies (f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i) )assume A9:
f = f1 . i
;
:: thesis: (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 18;
reconsider Fi =
(Fix_inp iv) . i as
Function ;
A10:
the
Sorts of
(FreeMSA the Sorts of A) . i <> {}
by A8;
Fi is
Function of
((FreeGen the Sorts of A) . i),
(the Sorts of (FreeMSA the Sorts of A) . i)
by A8, PBOOLE:def 18;
then A11:
dom Fi = (FreeGen the Sorts of A) . i
by A10, FUNCT_2:def 1;
A12:
(Fix_inp iv) . i c= g
by A7, A8, PBOOLE:def 5;
A13:
(Fix_inp iv) . i c= f
by A5, A8, A9, PBOOLE:def 5;
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 A11, A12, GRFUNC_1:64
.=
f | ((FreeGen the Sorts of A) . i)
by A11, A13, GRFUNC_1:64
;
:: thesis: 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:18; :: thesis: verum