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 not f is empty ; :: thesis: f = <*(f /. 1)*> ^ (f /^ 1)
then f | 1 = <*(f /. 1)*> by Th20;
hence f = <*(f /. 1)*> ^ (f /^ 1) by RFINSEQ:8; :: thesis: verum