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