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 ; :: according to TARSKI:def 3 :: thesis: ( not a in rng V or a in Union the Sorts of (Free (S,X)) )
assume a in rng V ; :: thesis: 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; :: thesis: verum

end;

then reconsider V = V as FinSequence of Union the Sorts of (Free (S,X)) by FINSEQ_1:def 4;
take V ; :: thesis: V is B -sorts
thus dom V = dom B by PARTFUN1:def 2; :: according to MSAFREE5:def 37 :: thesis: 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; :: thesis: ( i in dom B implies V . i in the Sorts of (Free (S,X)) . (B . i) )
assume A4: i in dom B ; :: thesis: 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; :: thesis: verum