let D be set ; :: thesis: for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( m in dom f & (f | n) /. m = f /. m )
let f be FinSequence of D; :: thesis: for n, m being Nat st n in dom f & m in Seg n holds
( m in dom f & (f | n) /. m = f /. m )
let n, m be Nat; :: thesis: ( n in dom f & m in Seg n implies ( m in dom f & (f | n) /. m = f /. m ) )
assume that
A1: n in dom f and
A2: m in Seg n ; :: thesis: ( m in dom f & (f | n) /. m = f /. m )
( dom f = Seg (len f) & n <= len f ) by A1, FINSEQ_1:def 3, FINSEQ_3:25;
then A3: Seg n c= dom f by FINSEQ_1:5;
hence m in dom f by A2; :: thesis: (f | n) /. m = f /. m
A4: Seg n = (dom f) /\ (Seg n) by A3, XBOOLE_1:28
.= dom (f | n) by RELAT_1:61 ;
hence (f | n) /. m = (f | n) . m by A2, PARTFUN1:def 6
.= f . m by A2, A4, FUNCT_1:47
.= f /. m by A2, A3, PARTFUN1:def 6 ;
:: thesis: verum