let f be non empty FinSequence; :: thesis: f = <*(f . 1)*> ^ (f /^ 1)
f | 1 = <*(f . 1)*> by Th20;
hence f = <*(f . 1)*> ^ (f /^ 1) by RFINSEQ:8; :: thesis: verum