set V = the Element of product ( the Sorts of (Free (S,X)) * B);
A0:
( rng B c= the carrier of S & the carrier of S = dom the Sorts of (Free (S,X)) )
by FINSEQ_1:def 4, PARTFUN1:def 2;
A1:
dom ( the Sorts of (Free (S,X)) * B) = dom B
by PARTFUN1:def 2;
A2:
( dom the Element of product ( the Sorts of (Free (S,X)) * B) = dom B & dom B = Seg (len B) )
by PARTFUN1:def 2, FINSEQ_1:def 3;
then reconsider V = the Element of product ( the Sorts of (Free (S,X)) * B) as FinSequence by FINSEQ_1:def 2;
rng V c= Union the Sorts of (Free (S,X))
proof
let a be
object ;
TARSKI:def 3 ( not a in rng V or a in Union the Sorts of (Free (S,X)) )
assume
a in rng V
;
a in Union the Sorts of (Free (S,X))
then consider i being
object such that A3:
(
i in dom V &
a = V . i )
by FUNCT_1:def 3;
reconsider i =
i as
Nat by A3;
( the Sorts of (Free (S,X)) * B) . i = the
Sorts of
(Free (S,X)) . (B . i)
by A2, A3, FUNCT_1:13;
then
(
V . i in the
Sorts of
(Free (S,X)) . (B . i) &
B . i in the
carrier of
S )
by A1, A2, A3, CARD_3:9, FUNCT_1:102;
hence
a in Union the
Sorts of
(Free (S,X))
by A0, A3, CARD_5:2;
verum
end;
then reconsider V = V as FinSequence of Union the Sorts of (Free (S,X)) by FINSEQ_1:def 4;
take
V
; V is B -sorts
thus
dom V = dom B
by PARTFUN1:def 2; MSAFREE5:def 37 for i being Nat st i in dom B holds
V . i in the Sorts of (Free (S,X)) . (B . i)
let i be Nat; ( i in dom B implies V . i in the Sorts of (Free (S,X)) . (B . i) )
assume A4:
i in dom B
; V . i in the Sorts of (Free (S,X)) . (B . i)
then
( the Sorts of (Free (S,X)) * B) . i = the Sorts of (Free (S,X)) . (B . i)
by FUNCT_1:13;
hence
V . i in the Sorts of (Free (S,X)) . (B . i)
by A1, A4, CARD_3:9; verum