deffunc H1( Element of dom B) -> Element of the Sorts of (Free (S,X)) . (B . S) = (V . S) -term ;
consider C being non empty FinSequence such that
A1: ( dom C = dom B & ( for i being Element of dom B holds C . i = H1(i) ) ) from MSAFREE5:sch 6();
 rng C c= Union the Sorts of (Free (S,X))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng C or a in Union the Sorts of (Free (S,X)) )
assume a in rng C ; :: thesis: a in Union the Sorts of (Free (S,X))
then consider i being object such that
A3: ( i in dom C & a = C . i ) by FUNCT_1:def 3;
reconsider i = i as Element of dom B by A1, A3;
reconsider t = (V . i) -term as Element of (Free (S,X)) ;
( C . i = t & the_sort_of t = B . i ) by A1, SORT;
hence a in Union the Sorts of (Free (S,X)) by A3; :: thesis: verum
end;
then reconsider C = C as FinSequence of Union the Sorts of (Free (S,X)) by FINSEQ_1:def 4;
take C ; :: thesis: C is V -context-sequence
thus dom C = dom B by A1; :: according to MSAFREE5:def 38 :: thesis: for i being Element of dom B holds C . i is context of V . i
let i be Element of dom B; :: thesis: C . i is context of V . i
C . i = (V . i) -term by A1;
hence C . i is context of V . i ; :: thesis: verum