let n, k 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: n c= dom p by A1, NAT_1:40;
then n = (dom p) /\ n by XBOOLE_1:28
.= dom (p | n) by RELAT_1:90 ;
hence ( (p | n) . k = p . k & k in dom p ) by A2, A3, FUNCT_1:70; :: thesis: verum