let D be non empty set ; :: thesis: for f being FinSequence of D st len f = 1 holds
f = <*(f /. 1)*>
let f be FinSequence of D; :: thesis: ( len f = 1 implies f = <*(f /. 1)*> )
assume A1: len f = 1 ; :: thesis: f = <*(f /. 1)*>
then not f is empty ;
then 1 in dom f by Th6;
then f . 1 = f /. 1 by PARTFUN1:def 8;
hence f = <*(f /. 1)*> by A1, FINSEQ_1:57; :: thesis: verum