let S be 1-sorted ; :: thesis: for p being FinSequence st ( for i being Nat st i in dom p holds

p . i in S ) holds

p is FinSequence of S

let p be FinSequence; :: thesis: ( ( for i being Nat st i in dom p holds

p . i in S ) implies p is FinSequence of S )

assume A1: for i being Nat st i in dom p holds

p . i in S ; :: thesis: p is FinSequence of S

for i being Nat st i in dom p holds

p . i in the carrier of S by A1, STRUCT_0:def 5;

hence p is FinSequence of S by FINSEQ_2:12; :: thesis: verum

p . i in S ) holds

p is FinSequence of S

let p be FinSequence; :: thesis: ( ( for i being Nat st i in dom p holds

p . i in S ) implies p is FinSequence of S )

assume A1: for i being Nat st i in dom p holds

p . i in S ; :: thesis: p is FinSequence of S

for i being Nat st i in dom p holds

p . i in the carrier of S by A1, STRUCT_0:def 5;

hence p is FinSequence of S by FINSEQ_2:12; :: thesis: verum