set I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } ;
{ xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } c= dom t
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } or a in dom t )
assume a in { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } ; :: thesis: a in dom t
then ex xi being Element of dom t st
( a = xi & ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] ) ;
hence a in dom t ; :: thesis: verum
end;
then consider f being FinSequence such that
A1: ( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & f is one-to-one ) by FINSEQ_4:58;
reconsider f = f as one-to-one FinSequence by A1;
deffunc H1( object ) -> set = t . (f . $1);
consider V being FinSequence such that
A2: ( len V = len f & ( for i being Nat st i in dom V holds
V . i = H1(i) ) ) from FINSEQ_1:sch 2();
 take V ; :: thesis: ex f being one-to-one FinSequence st
( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom V = dom f & ( for i being Nat st i in dom V holds
V . i = t . (f . i) ) )
take f ; :: thesis: ( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom V = dom f & ( for i being Nat st i in dom V holds
V . i = t . (f . i) ) )
thus rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } by A1; :: thesis: ( dom V = dom f & ( for i being Nat st i in dom V holds
V . i = t . (f . i) ) )
thus dom V = dom f by A2, FINSEQ_3:29; :: thesis: for i being Nat st i in dom V holds
V . i = t . (f . i)
thus for i being Nat st i in dom V holds
V . i = t . (f . i) by A2; :: thesis: verum