let x be set ; :: 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 Th55, FINSEQ_1:61;
thus apply <*f,g,h*>,x = apply (<*f,g*> ^ <*h*>),x by FINSEQ_1:60
.= <*x,(f . x),(g . (f . x))*> ^ <*(h . (<*x,(f . x),(g . (f . x))*> . (2 + 1)))*> by A1, Th44
.= <*x,(f . x),(g . (f . x))*> ^ <*(h . (g . (f . x)))*> by FINSEQ_1:62
.= (<*x*> ^ <*(f . x),(g . (f . x))*>) ^ <*(h . (g . (f . x)))*> by FINSEQ_1:60
.= <*x*> ^ (<*(f . x),(g . (f . x))*> ^ <*(h . (g . (f . x)))*>) by FINSEQ_1:45
.= <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*> by FINSEQ_1:60 ; :: thesis: verum