let f be XFinSequence; :: thesis: for n, m being Nat st n <= len f & m in n holds
( (f | n) . m = f . m & m in dom f )
let n, m be Nat; :: thesis: ( n <= len f & m in n implies ( (f | n) . m = f . m & m in dom f ) )
assume that
A1: n <= len f and
A2: m in n ; :: thesis: ( (f | n) . m = f . m & m in dom f )
A3: n c= dom f by A1, NAT_1:40;
then n = (dom f) /\ n by XBOOLE_1:28
.= dom (f | n) by RELAT_1:90 ;
hence ( (f | n) . m = f . m & m in dom f ) by A2, A3, FUNCT_1:70; :: thesis: verum