set V = the Element of product (X * B);
A0: ( rng B c= the carrier of S & the carrier of S = dom X ) by FINSEQ_1:def 4, PARTFUN1:def 2;
A1: dom (X * B) = dom B by PARTFUN1:def 2;
A2: ( dom the Element of product (X * B) = dom B & dom B = Seg (len B) ) by PARTFUN1:def 2, FINSEQ_1:def 3;
then reconsider V = the Element of product (X * B) as FinSequence by FINSEQ_1:def 2;
rng V c= Union X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng V or a in Union X )
assume a in rng V ; :: thesis: a in Union 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;
(X * B) . i = X . (B . i) by A2, A3, FUNCT_1:13;
then ( V . i in X . (B . i) & B . i in the carrier of S ) by A1, A2, A3, CARD_3:9, FUNCT_1:102;
hence a in Union X by A0, A3, CARD_5:2; :: thesis: verum

end;

then reconsider V = V as FinSequence of Union 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 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 A4: i in dom B ; :: thesis: V . i in X . (B . i)
then (X * B) . i = X . (B . i) by FUNCT_1:13;
hence V . i in X . (B . i) by A1, A4, CARD_3:9; :: thesis: verum