defpred S1[ set , set , set ] means $3 = root-tree [$2,$1];
let IT1, IT2 be ManySortedFunction of (FreeEnv MSA),MSA; ( 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 IT19 = IT1, IT29 = IT2 as ManySortedFunction of (FreeMSA the Sorts of MSA),MSA ;
assume
IT1 is_homomorphism FreeEnv MSA,MSA
; ( 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:
IT19 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
; ( 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 )
A15:
for s being SortSymbol of S
for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT19 . s) . y = x iff S1[s,x,y] )
proof
let s be
SortSymbol of
S;
for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT19 . s) . y = x iff S1[s,x,y] )let x,
y be
set ;
( y in FreeGen (s, the Sorts of MSA) implies ( (IT19 . s) . y = x iff S1[s,x,y] ) )
assume A16:
y in FreeGen (
s, the
Sorts of
MSA)
;
( (IT19 . s) . y = x iff S1[s,x,y] )
then consider a being
set such that A17:
a in the
Sorts of
MSA . s
and A18:
y = root-tree [a,s]
by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA) . s
by A16;
then A19:
y in FreeSort ( the
Sorts of
MSA,
s)
by MSAFREE:def 11;
hence
(
(IT19 . s) . y = x implies
y = root-tree [x,s] )
by A14, A17, A18;
( S1[s,x,y] implies (IT19 . s) . y = x )
assume
y = root-tree [x,s]
;
(IT19 . s) . y = x
then
[x,s] = [a,s]
by A18, TREES_4:4;
then
x = a
by XTUPLE_0:1;
hence
(IT19 . s) . y = x
by A14, A19, A17, A18;
verum
end;
assume
IT2 is_homomorphism FreeEnv MSA,MSA
; ( 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:
IT29 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
; IT1 = IT2
A22:
for s being SortSymbol of S
for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT29 . s) . y = x iff S1[s,x,y] )
proof
let s be
SortSymbol of
S;
for x, y being set st y in FreeGen (s, the Sorts of MSA) holds
( (IT29 . s) . y = x iff S1[s,x,y] )let x,
y be
set ;
( y in FreeGen (s, the Sorts of MSA) implies ( (IT29 . s) . y = x iff S1[s,x,y] ) )
assume A23:
y in FreeGen (
s, the
Sorts of
MSA)
;
( (IT29 . s) . y = x iff S1[s,x,y] )
then consider a being
set such that A24:
a in the
Sorts of
MSA . s
and A25:
y = root-tree [a,s]
by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA) . s
by A23;
then A26:
y in FreeSort ( the
Sorts of
MSA,
s)
by MSAFREE:def 11;
hence
(
(IT29 . s) . y = x implies
y = root-tree [x,s] )
by A21, A24, A25;
( S1[s,x,y] implies (IT29 . s) . y = x )
assume
y = root-tree [x,s]
;
(IT29 . s) . y = x
then
[x,s] = [a,s]
by A25, TREES_4:4;
then
x = a
by XTUPLE_0:1;
hence
(IT29 . s) . y = x
by A21, A26, A24, A25;
verum
end;
IT19 = IT29
from MSAFREE1:sch 3(A13, A15, A20, A22);
hence
IT1 = IT2
; verum