let x be set ; :: thesis: for p, q being Function-yielding FinSequence holds (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)
let p, q be Function-yielding FinSequence; :: thesis: (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)
defpred S₁[ Function-yielding FinSequence] means (apply (p ^ $1),x) . ((len (p ^ $1)) + 1) = (apply $1,((apply p,x) . ((len p) + 1))) . ((len $1) + 1);
A1: for p being Function-yielding FinSequence st S₁[p] holds
for f being Function holds S₁[p ^ <*f*>]

proof

set y = (apply p,x) . ((len p) + 1);
let q be Function-yielding FinSequence; :: thesis: ( S₁[q] implies for f being Function holds S₁[q ^ <*f*>] )
assume A2: (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1) ; :: thesis: for f being Function holds S₁[q ^ <*f*>]
let f be Function; :: thesis: S₁[q ^ <*f*>]
A3: len <*f*> = 1 by FINSEQ_1:57;
then A4: len ((p ^ q) ^ <*f*>) = (len (p ^ q)) + 1 by FINSEQ_1:35;
A5: len (q ^ <*f*>) = (len q) + 1 by A3, FINSEQ_1:35;
A6: ( apply (q ^ <*f*>),((apply p,x) . ((len p) + 1)) = (apply q,((apply p,x) . ((len p) + 1))) ^ <*(f . ((apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)))*> & len (apply q,((apply p,x) . ((len p) + 1))) = (len q) + 1 ) by Def5, Th44;
A7: len (apply (p ^ q),x) = (len (p ^ q)) + 1 by Def5;
( p ^ (q ^ <*f*>) = (p ^ q) ^ <*f*> & apply ((p ^ q) ^ <*f*>),x = (apply (p ^ q),x) ^ <*(f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1)))*> ) by Th44, FINSEQ_1:45;
hence (apply (p ^ (q ^ <*f*>)),x) . ((len (p ^ (q ^ <*f*>))) + 1) = f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1)) by A7, A4, FINSEQ_1:59
.= (apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) . ((len (q ^ <*f*>)) + 1) by A2, A6, A5, FINSEQ_1:59 ;
:: thesis: verum

end;

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