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
for B being FinSequence of the carrier of S st B = pr2 f holds
pr1 f is b₄ -sorts FinSequence of Union X
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
for B being FinSequence of the carrier of S st B = pr2 f holds
pr1 f is b₃ -sorts FinSequence of Union X
let t be Element of (Free (S,X)); :: thesis: for f being vf-sequence of t
for B being FinSequence of the carrier of S st B = pr2 f holds
pr1 f is b₂ -sorts FinSequence of Union X
let f be vf-sequence of t; :: thesis: for B being FinSequence of the carrier of S st B = pr2 f holds
pr1 f is b₁ -sorts FinSequence of Union X
let B be FinSequence of the carrier of S; :: thesis: ( B = pr2 f implies pr1 f is B -sorts FinSequence of Union X )
assume Z0: B = pr2 f ; :: thesis: pr1 f is B -sorts FinSequence of Union X
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;
pr1 f is FinSequence of Union X

proof

let a be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not a in proj2 (pr1 f) or a in Union X )
assume a in rng (pr1 f) ; :: thesis: a in Union X
then consider b being object such that
A2: ( b in dom (pr1 f) & a = (pr1 f) . b ) by FUNCT_1:def 3;
reconsider b = b as Nat by A2;
A3: dom (pr1 f) = dom f by MCART_1:def 12;
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) `1 by A2, A3, MCART_1:def 12
.= [x,s] `1 by A1, A2, A3, A4, A5 ;
hence a in Union X ; :: thesis: verum

end;

then reconsider V = pr1 f as FinSequence of Union X ;
V is B -sorts

proof

A6: ( dom V = dom f & dom f = dom B ) by Z0, MCART_1:def 12, MCART_1:def 13;
hence dom V = dom B ; :: according to MSAFREE5:def 36 :: thesis: for i being Nat st i in dom B holds
V . i in X . (B . i)
let i be Nat; :: thesis: ( i in dom B implies V . i in X . (B . i) )
assume A7: i in dom B ; :: thesis: V . i in X . (B . i)
then g . i in rng g by A1, A6, FUNCT_1:def 3;
then consider xi being Element of dom t such that
A4: ( g . i = 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;
( B . i = (f . i) `2 & V . i = (f . i) `1 & f . i = [x,s] ) by Z0, A1, A4, A5, A6, A7, MCART_1:def 12, MCART_1:def 13;
hence V . i in X . (B . i) ; :: thesis: verum

end;

hence pr1 f is B -sorts FinSequence of Union X ; :: thesis: verum