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