let S be non empty non void ManySortedSign ; for X being V5() 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 b4 -sorts FinSequence of Union X
let X be V5() 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 b3 -sorts FinSequence of Union X
let t be 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 b2 -sorts FinSequence of Union X
let f be vf-sequence of t; for B being FinSequence of the carrier of S st B = pr2 f holds
pr1 f is b1 -sorts FinSequence of Union X
let B be FinSequence of the carrier of S; ( B = pr2 f implies pr1 f is B -sorts FinSequence of Union X )
assume Z0:
B = pr2 f
; 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 ;
TARSKI:def 3,
FINSEQ_1:def 4 ( not a in proj2 (pr1 f) or a in Union X )
assume
a in rng (pr1 f)
;
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
;
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
;
MSAFREE5:def 36 for i being Nat st i in dom B holds
V . i in X . (B . i)
let i be
Nat;
( i in dom B implies V . i in X . (B . i) )
assume A7:
i in dom B
;
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)
;
verum
end;
hence
pr1 f is B -sorts FinSequence of Union X
; verum