let IT be FinSequence of A; :: thesis:
A3: len ll = k by CARD_1:def 7;
dom v = bound_QC-variables Al by FUNCT_2:def 1;
then A4: rng ll c= dom v by RELAT_1:def 19;
thus ( IT = v * ll implies ( len IT = k & ( for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) ) ) :: thesis:

end;

assume that
A7: len IT = k and
A8: for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i) ; :: thesis:
A9: for x being object holds
( x in dom IT iff ( x in dom ll & ll . x in dom v ) )

let x be object ; :: thesis:
thus ( x in dom IT implies ( x in dom ll & ll . x in dom v ) ) :: thesis:

end;

end;

for x being object st x in dom IT holds
IT . x = v . (ll . x)

let x be object ; :: thesis:
assume A11: x in dom IT ; :: thesis:
then reconsider i = x as Element of NAT ;
( 1 <= i & i <= k ) by A7, A11, FINSEQ_3:25;
hence IT . x = v . (ll . x) by A8; :: thesis:

end;