let x be object ; :: 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 ;
A2: ( apply ({},x) = <*x*> & len {} = 0 ) by Th39;
thus apply (<*f*>,x) = apply (({} ^ <*f*>),x) by FINSEQ_1:34
.= <*x*> ^ <*(f . x)*> by A2, A1, Th41
.= <*x,(f . x)*> by FINSEQ_1:def 9 ; :: thesis: verum