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