defpred S1[ object ] means ex a being set st
( a in X . s & $1 = root-tree [a,s] );
set D = DTConMSA X;
consider A being set such that
A1:
for x being object holds
( x in A iff ( x in (FreeSort X) . s & S1[x] ) )
from XBOOLE_0:sch 1();
A c= (FreeSort X) . s
by A1;
then reconsider A = A as Subset of ((FreeSort X) . s) ;
for x being set holds
( x in A iff S1[x] )
proof
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . s in rng (coprod X)
by FUNCT_1:def 3;
then A2:
coprod (
s,
X)
in rng (coprod X)
by Def3;
A3:
Terminals (DTConMSA X) = Union (coprod X)
by Th6;
let x be
set ;
( x in A iff S1[x] )
thus
(
x in A implies
S1[
x] )
by A1;
( S1[x] implies x in A )
set A =
{ aa where aa is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) ) } ;
assume A4:
S1[
x]
;
x in A
then consider a being
set such that A5:
a in X . s
and A6:
x = root-tree [a,s]
;
A7:
(FreeSort X) . s = FreeSort (
X,
s)
by Def11;
set sa =
[a,s];
[a,s] in coprod (
s,
X)
by A5, Def2;
then
[a,s] in union (rng (coprod X))
by A2, TARSKI:def 4;
then A8:
[a,s] in Terminals (DTConMSA X)
by A3, CARD_3:def 4;
then reconsider sa =
[a,s] as
Symbol of
(DTConMSA X) ;
reconsider b =
root-tree sa as
Element of
TS (DTConMSA X) by A8, DTCONSTR:def 1;
b in { aa where aa is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) ) }
by A5;
hence
x in A
by A1, A4, A6, A7;
verum
end;
hence
ex b1 being Subset of ((FreeSort X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) )
; verum