let z be object ; for p being XFinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )
let p be XFinSequence; ( z in p implies ex k being Nat st
( k in dom p & z = [k,(p . k)] ) )
assume A1:
z in p
; 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 Element of NAT ;
take
k
; ( k in dom p & z = [k,(p . k)] )
thus
( k in dom p & z = [k,(p . k)] )
by A1, A2, FUNCT_1:1; verum