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: <*x*> . (0 + 1) = x by FINSEQ_1:57;
A2: ( apply {} ,x = <*x*> & len {} = 0 ) by Th42;
thus apply <*f*>,x = apply ({} ^ <*f*>),x by FINSEQ_1:47
.= <*x*> ^ <*(f . x)*> by A2, A1, Th44
.= <*x,(f . x)*> by FINSEQ_1:def 9 ; :: thesis: verum