let x be object ; :: thesis: for f, g, h being Function holds apply (<*f,g,h*>,x) = <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*>
let f, g, h be Function; :: thesis: apply (<*f,g,h*>,x) = <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*>
A1: ( apply (<*f,g*>,x) = <*x,(f . x),(g . (f . x))*> & len <*f,g*> = 2 ) by Th52, FINSEQ_1:44;
thus apply (<*f,g,h*>,x) = apply ((<*f,g*> ^ <*h*>),x) by FINSEQ_1:43
.= <*x,(f . x),(g . (f . x))*> ^ <*(h . (<*x,(f . x),(g . (f . x))*> . (2 + 1)))*> by A1, Th41
.= <*x,(f . x),(g . (f . x))*> ^ <*(h . (g . (f . x)))*>
.= (<*x*> ^ <*(f . x),(g . (f . x))*>) ^ <*(h . (g . (f . x)))*> by FINSEQ_1:43
.= <*x*> ^ (<*(f . x),(g . (f . x))*> ^ <*(h . (g . (f . x)))*>) by FINSEQ_1:32
.= <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*> by FINSEQ_1:43 ; :: thesis: verum