let IT be FinSequence of A; :: thesis: ( IT = *' iff ( len IT = k & ( for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) ) )
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: ( len IT = k & ( for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) implies IT = *' )

proof

assume A5: IT = v * ll ; :: thesis: ( len IT = k & ( for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) )
then A6: dom ll = dom IT by A4, RELAT_1:27;
hence len IT = k by A3, FINSEQ_3:29; :: thesis: for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i)
let i be Nat; :: thesis: ( 1 <= i & i <= k implies IT . i = v . (ll . i) )
assume ( 1 <= i & i <= k ) ; :: thesis: IT . i = v . (ll . i)
then i in dom IT by A3, A6, FINSEQ_3:25;
hence IT . i = v . (ll . i) by A5, FUNCT_1:12; :: thesis: verum

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: IT = *'
A9: for x being object holds
( x in dom IT iff ( x in dom ll & ll . x in dom v ) )

proof

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

proof

assume x in dom IT ; :: thesis: ( x in dom ll & ll . x in dom v )
hence x in dom ll by A3, A7, FINSEQ_3:29; :: thesis: ll . x in dom v
then ll . x in rng ll by FUNCT_1:def 3;
hence ll . x in dom v by A4; :: thesis: verum

end;

assume that
A10: x in dom ll and
ll . x in dom v ; :: thesis: x in dom IT
thus x in dom IT by A3, A7, A10, FINSEQ_3:29; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in dom IT implies IT . x = v . (ll . x) )
assume A11: x in dom IT ; :: thesis: IT . x = v . (ll . x)
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: verum

end;

hence IT = *' by A9, FUNCT_1:10; :: thesis: verum