let z be object ; :: thesis: for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )
let p be FinSequence; :: thesis: ( z in p implies ex k being Nat st
( k in dom p & z = [k,(p . k)] ) )
assume A1: z in p ; :: thesis: ex k being Nat st
( k in dom p & z = [k,(p . k)] )
then consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
x in dom p by A1, A2, FUNCT_1:1;
then reconsider k = x as Nat ;
take k ; :: thesis: ( k in dom p & z = [k,(p . k)] )
thus ( k in dom p & z = [k,(p . k)] ) by A1, A2, FUNCT_1:1; :: thesis: verum