let x be set ; :: thesis: for p, q being Function-yielding FinSequence holds apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1)))
let p, q be Function-yielding FinSequence; :: thesis: apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1)))
defpred S₁[ Function-yielding FinSequence] means apply (p ^ $1),x = (apply p,x) $^ (apply $1,((apply p,x) . ((len p) + 1)));
A1: len (apply p,x) = (len p) + 1 by Def5;
then consider r being FinSequence, y being set such that
A2: apply p,x = r ^ <*y*> by CARD_1:47, FINSEQ_1:63;
A3: for p being Function-yielding FinSequence st S₁[p] holds
for f being Function holds S₁[p ^ <*f*>]

proof

let q be Function-yielding FinSequence; :: thesis: ( S₁[q] implies for f being Function holds S₁[q ^ <*f*>] )
assume A4: apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1))) ; :: thesis: for f being Function holds S₁[q ^ <*f*>]
A5: (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1) by Th51;
let f be Function; :: thesis: S₁[q ^ <*f*>]
A6: len (apply q,((apply p,x) . ((len p) + 1))) = (len q) + 1 by Def5;
A7: len (apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) = (len (q ^ <*f*>)) + 1 by Def5;
thus apply (p ^ (q ^ <*f*>)),x = apply ((p ^ q) ^ <*f*>),x by FINSEQ_1:45
.= (apply (p ^ q),x) ^ <*(f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1)))*> by Th44
.= (r ^ (apply q,((apply p,x) . ((len p) + 1)))) ^ <*(f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1)))*> by A2, A4, A6, CARD_1:47, REWRITE1:2
.= r ^ ((apply q,((apply p,x) . ((len p) + 1))) ^ <*(f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1)))*>) by FINSEQ_1:45
.= r ^ (apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) by A5, Th44
.= (apply p,x) $^ (apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) by A2, A7, CARD_1:47, REWRITE1:2 ; :: thesis: verum

end;

len <*y*> = 1 by FINSEQ_1:57;
then (len p) + 1 = (len r) + 1 by A1, A2, FINSEQ_1:35;
then A8: (apply p,x) . ((len p) + 1) = y by A2, FINSEQ_1:59;
apply (p ^ {} ),x = apply p,x by FINSEQ_1:47
.= (apply p,x) $^ <*((apply p,x) . ((len p) + 1))*> by A2, A8, REWRITE1:2
.= (apply p,x) $^ (apply {} ,((apply p,x) . ((len p) + 1))) by Th42 ;
then A9: S₁[ {} ] ;
for q being Function-yielding FinSequence holds S₁[q] from FUNCT_7:sch 5(A9, A3);
hence apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1))) ; :: thesis: verum