let f be non empty FinSequence; :: thesis: f /^ 1 = Del (f,1)
consider i being Nat such that
A1: i + 1 = len f by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
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: len (f /^ 1) = (i + 1) - 1 by A1, A2, RFINSEQ:def 1
.= i ;
1 in dom f by Th6;
hence len (f /^ 1) = len (Del (f,1)) by A1, A3, FINSEQ_3:109; :: thesis: for k being Nat st 1 <= k & k <= len (f /^ 1) holds
(f /^ 1) . k = (Del (f,1)) . k
A4: 1 in dom f by Th6;
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
k in dom (f /^ 1) by A5, FINSEQ_3:25;
hence (f /^ 1) . k = f . (k + 1) by A2, RFINSEQ:def 1
.= (Del (f,1)) . k by A1, A3, A5, A4, FINSEQ_3:111 ;
:: thesis: verum

end;

hence f /^ 1 = Del (f,1) ; :: thesis: verum