let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for f being vf-sequence of t holds pr2 f is FinSequence of the carrier of S
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for f being vf-sequence of t holds pr2 f is FinSequence of the carrier of S
let t be Element of (Free (S,X)); :: thesis: for f being vf-sequence of t holds pr2 f is FinSequence of the carrier of S
let f be vf-sequence of t; :: thesis: pr2 f is FinSequence of the carrier of S
consider g being one-to-one FinSequence such that
A1: ( rng g = { 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 f = dom g & ( for i being Nat st i in dom f holds
f . i = t . (g . i) ) ) by VFS;
let a be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not a in proj2 (pr2 f) or a in the carrier of S )
assume a in rng (pr2 f) ; :: thesis: a in the carrier of S
then consider b being object such that
A2: ( b in dom (pr2 f) & a = (pr2 f) . b ) by FUNCT_1:def 3;
reconsider b = b as Nat by A2;
A3: dom (pr2 f) = dom f by MCART_1:def 13;
then g . b in rng g by A1, A2, FUNCT_1:def 3;
then consider xi being Element of dom t such that
A4: ( g . b = xi & ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] ) by A1;
consider s being SortSymbol of S, x being Element of X . s such that
A5: t . xi = [x,s] by A4;
a = (f . b) `2 by A2, A3, MCART_1:def 13
.= [x,s] `2 by A1, A2, A3, A4, A5
.= s ;
hence a in the carrier of S ; :: thesis: verum