let f be non empty FinSequence; :: thesis: f = <*(f . 1)*> ^ (Del (f,1))
thus f = <*(f . 1)*> ^ (f /^ 1) by Th29a
.= <*(f . 1)*> ^ (Del (f,1)) by Th3 ; :: thesis: verum