let x be set ; :: thesis: for f being Function holds apply <*f*>,x = <*x,(f . x)*>
let f be Function; :: thesis: apply <*f*>,x = <*x,(f . x)*>
A1: ( apply {} ,x = <*x*> & len {} = 0 & <*x*> . (0 + 1) = x ) by Th42, FINSEQ_1:57;
thus apply <*f*>,x = apply ({} ^ <*f*>),x by FINSEQ_1:47
.= <*x*> ^ <*(f . x)*> by A1, Th44
.= <*x,(f . x)*> by FINSEQ_1:def 9 ; :: thesis: verum