let x be object ; :: thesis: for f, g being Function holds apply (<*f,g*>,x) = <*x,(f . x),(g . (f . x))*>
let f, g be Function; :: thesis: apply (<*f,g*>,x) = <*x,(f . x),(g . (f . x))*>
A1: ( apply (<*f*>,x) = <*x,(f . x)*> & len <*f*> = 1 ) by Th46, FINSEQ_1:40;
thus apply (<*f,g*>,x) = apply ((<*f*> ^ <*g*>),x) by FINSEQ_1:def 9
.= <*x,(f . x)*> ^ <*(g . (<*x,(f . x)*> . (1 + 1)))*> by A1, Th41
.= <*x,(f . x)*> ^ <*(g . (f . x))*>
.= <*x,(f . x),(g . (f . x))*> by FINSEQ_1:43 ; :: thesis: verum