let x be set ; :: 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 Th49, FINSEQ_1:57;
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, Th44
.= <*x,(f . x)*> ^ <*(g . (f . x))*> by FINSEQ_1:61
.= <*x,(f . x),(g . (f . x))*> by FINSEQ_1:60 ; :: thesis: verum