let k, n be Nat; :: thesis: for p being XFinSequence st n <= len p & k in n holds
( (p | n) . k = p . k & k in dom p )
let p be XFinSequence; :: thesis: ( n <= len p & k in n implies ( (p | n) . k = p . k & k in dom p ) )
assume that
A1: n <= len p and
A2: k in n ; :: thesis: ( (p | n) . k = p . k & k in dom p )
A3: Segm n c= Segm (len p) by A1, NAT_1:39;
then n = (dom p) /\ n by XBOOLE_1:28
.= dom (p | n) by RELAT_1:61 ;
hence ( (p | n) . k = p . k & k in dom p ) by A2, A3, FUNCT_1:47; :: thesis: verum