let D be set ; 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; 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; ( 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
; ( 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; (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
;
verum