let D be non empty set ; :: thesis: for f being non empty FinSequence of D holds f /^ 1 = Del f,1
let f be non empty FinSequence of D; :: thesis: f /^ 1 = Del f,1
consider i being Nat such that
A1: i + 1 = len f by FINSEQ_5:7;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A2: 1 <= len f by A1, NAT_1:11;
( len (f /^ 1) = len (Del f,1) & ( for k being Nat st 1 <= k & k <= len (f /^ 1) holds
(f /^ 1) . k = (Del f,1) . k ) )

proof

A3: 1 in dom f by FINSEQ_5:6;
A4: len (f /^ 1) = (i + 1) - 1 by A1, A2, RFINSEQ:def 2
.= i ;
hence len (f /^ 1) = len (Del f,1) by A1, A3, FINSEQ_3:118; :: thesis: for k being Nat st 1 <= k & k <= len (f /^ 1) holds
(f /^ 1) . k = (Del f,1) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len (f /^ 1) implies (f /^ 1) . k = (Del f,1) . k )
assume A5: ( 1 <= k & k <= len (f /^ 1) ) ; :: thesis: (f /^ 1) . k = (Del f,1) . k
A6: ( 1 in dom f & 1 <= k & k <= i ) by A4, A5, FINSEQ_5:6;
A7: k in dom (f /^ 1) by A5, FINSEQ_3:27;
hence (f /^ 1) . k = f . (k + 1) by A2, RFINSEQ:def 2
.= (Del f,1) . k by A1, A6, A7, FINSEQ_3:120 ;
:: thesis: verum

end;

hence f /^ 1 = Del f,1 by FINSEQ_1:18; :: thesis: verum