let V be non empty addLoopStr ; :: thesis: for F being FinSequence of the carrier of V
for k, n being Element of NAT st k in Seg n & len F = n holds
F . k is Element of V
let F be FinSequence of the carrier of V; :: thesis: for k, n being Element of NAT st k in Seg n & len F = n holds
F . k is Element of V
let k, n be Element of NAT ; :: thesis: ( k in Seg n & len F = n implies F . k is Element of V )
assume ( k in Seg n & len F = n ) ; :: thesis: F . k is Element of V
then k in dom F by FINSEQ_1:def 3;
then ( F . k in rng F & rng F c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:def 5;
hence F . k is Element of V ; :: thesis: verum