let S be 1-sorted ; :: thesis: for i being Element of NAT
for p being FinSequence of S st i in dom p holds
p . i in S
let i be Element of NAT ; :: thesis: for p being FinSequence of S st i in dom p holds
p . i in S
let p be FinSequence of S; :: thesis: ( i in dom p implies p . i in S )
assume i in dom p ; :: thesis: p . i in S
hence p . i in the carrier of S by FINSEQ_2:11; :: according to STRUCT_0:def 5 :: thesis: verum