let x be object ; for f, g being Function holds apply (<*f,g*>,x) = <*x,(f . x),(g . (f . x))*>
let f, g be Function; 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))*>
by FINSEQ_1:44
.=
<*x,(f . x),(g . (f . x))*>
by FINSEQ_1:43
; verum