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

proof

let i be Nat; :: thesis: ( i in dom p implies p . i in the carrier of S )
assume i in dom p ; :: thesis: p . i in the carrier of S
then p . i in S by A1;
hence p . i in the carrier of S by STRUCT_0:def 5; :: thesis: verum

end;

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