let IT1, IT2 be ManySortedFunction of (FreeEnv MSA),MSA; :: thesis: ( IT1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT1 . s) . y = x ) & IT2 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT2 . s) . y = x ) implies IT1 = IT2 )
reconsider IT1' = IT1, IT2' = IT2 as ManySortedFunction of (FreeMSA the Sorts of MSA),MSA ;
assume
IT1 is_homomorphism FreeEnv MSA,MSA
; :: thesis: ( ex s being SortSymbol of S ex x, y being set st
( y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT1 . s) . y = x ) or not IT2 is_homomorphism FreeEnv MSA,MSA or ex s being SortSymbol of S ex x, y being set st
( y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 )
then A13:
IT1' is_homomorphism FreeMSA the Sorts of MSA,MSA
;
assume A14:
for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT1 . s) . y = x
; :: thesis: ( not IT2 is_homomorphism FreeEnv MSA,MSA or ex s being SortSymbol of S ex x, y being set st
( y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 )
defpred S1[ set , set , set ] means $3 = root-tree [$2,$1];
A15:
for s being SortSymbol of S
for x, y being set st y in FreeGen s,the Sorts of MSA holds
( (IT1' . s) . y = x iff S1[s,x,y] )
proof
let s be
SortSymbol of
S;
:: thesis: for x, y being set st y in FreeGen s,the Sorts of MSA holds
( (IT1' . s) . y = x iff S1[s,x,y] )let x,
y be
set ;
:: thesis: ( y in FreeGen s,the Sorts of MSA implies ( (IT1' . s) . y = x iff S1[s,x,y] ) )
assume A16:
y in FreeGen s,the
Sorts of
MSA
;
:: thesis: ( (IT1' . s) . y = x iff S1[s,x,y] )
then
y in (FreeSort the Sorts of MSA) . s
;
then A17:
y in FreeSort the
Sorts of
MSA,
s
by MSAFREE:def 13;
consider a being
set such that A18:
a in the
Sorts of
MSA . s
and A19:
y = root-tree [a,s]
by A16, MSAFREE:def 17;
thus
(
(IT1' . s) . y = x implies
y = root-tree [x,s] )
by A14, A17, A18, A19;
:: thesis: ( S1[s,x,y] implies (IT1' . s) . y = x )
assume
y = root-tree [x,s]
;
:: thesis: (IT1' . s) . y = x
then
[x,s] = [a,s]
by A19, TREES_4:4;
then
x = a
by ZFMISC_1:33;
hence
(IT1' . s) . y = x
by A14, A17, A18, A19;
:: thesis: verum
end;
assume
IT2 is_homomorphism FreeEnv MSA,MSA
; :: thesis: ( ex s being SortSymbol of S ex x, y being set st
( y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s & not (IT2 . s) . y = x ) or IT1 = IT2 )
then A20:
IT2' is_homomorphism FreeMSA the Sorts of MSA,MSA
;
assume A21:
for s being SortSymbol of S
for x, y being set st y in FreeSort the Sorts of MSA,s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT2 . s) . y = x
; :: thesis: IT1 = IT2
A22:
for s being SortSymbol of S
for x, y being set st y in FreeGen s,the Sorts of MSA holds
( (IT2' . s) . y = x iff S1[s,x,y] )
proof
let s be
SortSymbol of
S;
:: thesis: for x, y being set st y in FreeGen s,the Sorts of MSA holds
( (IT2' . s) . y = x iff S1[s,x,y] )let x,
y be
set ;
:: thesis: ( y in FreeGen s,the Sorts of MSA implies ( (IT2' . s) . y = x iff S1[s,x,y] ) )
assume A23:
y in FreeGen s,the
Sorts of
MSA
;
:: thesis: ( (IT2' . s) . y = x iff S1[s,x,y] )
then
y in (FreeSort the Sorts of MSA) . s
;
then A24:
y in FreeSort the
Sorts of
MSA,
s
by MSAFREE:def 13;
consider a being
set such that A25:
a in the
Sorts of
MSA . s
and A26:
y = root-tree [a,s]
by A23, MSAFREE:def 17;
thus
(
(IT2' . s) . y = x implies
y = root-tree [x,s] )
by A21, A24, A25, A26;
:: thesis: ( S1[s,x,y] implies (IT2' . s) . y = x )
assume
y = root-tree [x,s]
;
:: thesis: (IT2' . s) . y = x
then
[x,s] = [a,s]
by A26, TREES_4:4;
then
x = a
by ZFMISC_1:33;
hence
(IT2' . s) . y = x
by A21, A24, A25, A26;
:: thesis: verum
end;
IT1' = IT2'
from MSAFREE1:sch 3(A13, A15, A20, A22);
hence
IT1 = IT2
; :: thesis: verum