let f be FinSequence; :: thesis: for n, m being Nat st n in dom f & m in Seg n holds

( (f | n) . m = f . m & m in dom f )

let n, m be Nat; :: thesis: ( n in dom f & m in Seg n implies ( (f | n) . m = f . m & m in dom f ) )

assume that

A1: n in dom f and

A2: m in Seg n ; :: thesis: ( (f | n) . m = f . m & m in dom f )

( dom f = Seg (len f) & n <= len f ) by A1, FINSEQ_1:def 3, FINSEQ_3:25;

then A4: Seg n c= dom f by FINSEQ_1:5;

then Seg n = (dom f) /\ (Seg n) by XBOOLE_1:28

.= dom (f | n) by RELAT_1:61 ;

hence ( (f | n) . m = f . m & m in dom f ) by A2, A4, FUNCT_1:47; :: thesis: verum

( (f | n) . m = f . m & m in dom f )

let n, m be Nat; :: thesis: ( n in dom f & m in Seg n implies ( (f | n) . m = f . m & m in dom f ) )

assume that

A1: n in dom f and

A2: m in Seg n ; :: thesis: ( (f | n) . m = f . m & m in dom f )

( dom f = Seg (len f) & n <= len f ) by A1, FINSEQ_1:def 3, FINSEQ_3:25;

then A4: Seg n c= dom f by FINSEQ_1:5;

then Seg n = (dom f) /\ (Seg n) by XBOOLE_1:28

.= dom (f | n) by RELAT_1:61 ;

hence ( (f | n) . m = f . m & m in dom f ) by A2, A4, FUNCT_1:47; :: thesis: verum