let k be Nat; :: thesis: for p being XFinSequence holds
( k < len p iff k in dom p )
let p be XFinSequence; :: thesis: ( k < len p iff k in dom p )
thus ( k < len p implies k in dom p ) :: thesis: ( k in dom p implies k < len p )

proof

assume k < len p ; :: thesis: k in dom p
then k in Segm (len p) by NAT_1:44;
hence k in dom p ; :: thesis: verum

end;

assume k in dom p ; :: thesis: k < len p
then k in Segm (len p) ;
hence k < len p by NAT_1:44; :: thesis: verum