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

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