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;
len <*y*> = 1 by FINSEQ_1:57;
then (len p) + 1 = (len r) + 1 by A1, A2, FINSEQ_1:35;
then A3: (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, A3, REWRITE1:2
.= (apply p,x) $^ (apply {} ,((apply p,x) . ((len p) + 1))) by Th42 ;
then A4: S₁[ {} ] ;
A5: 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 A6: apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1))) ; :: thesis: for f being Function holds S₁[q ^ <*f*>]
let f be Function; :: thesis: S₁[q ^ <*f*>]
B7: len (apply q,((apply p,x) . ((len p) + 1))) = (len q) + 1 by Def5;
B8: len (apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) = (len (q ^ <*f*>)) + 1 by Def5;
A9: (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1) by Th51;
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, A6, B7, 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 A9, Th44
.= (apply p,x) $^ (apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) by A2, B8, CARD_1:47, REWRITE1:2 ; :: thesis: verum

end;

for q being Function-yielding FinSequence holds S₁[q] from FUNCT_7:sch 5(A4, A5);
hence apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1))) ; :: thesis: verum