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 FINSEQ_5:6;
thus f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:32
.= <*(f . 1)*> ^ (f /^ 1) by A1, PARTFUN1:def 8
.= <*(f . 1)*> ^ (Del (f,1)) by Th3 ; :: thesis: verum