let D be non empty set ; :: thesis: for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))
let f be non empty FinSequence of D; :: thesis: f = <*(f . 1)*> ^ (Del (f,1))
A1: 1 in dom f by Th6;
thus f = <*(f /. 1)*> ^ (f /^ 1) by Th29
.= <*(f . 1)*> ^ (f /^ 1) by A1, PARTFUN1:def 6
.= <*(f . 1)*> ^ (Del (f,1)) by Th3 ; :: thesis: verum