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:40;
then A4: len ((p ^ q) ^ <*f*>) = (len (p ^ q)) + 1 by FINSEQ_1:22;
A5: len (q ^ <*f*>) = (len q) + 1 by A3, FINSEQ_1:22;
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:32;
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:42
.= (apply ((q ^ <*f*>),((apply (p,x)) . ((len p) + 1)))) . ((len (q ^ <*f*>)) + 1) by A2, A6, A5, FINSEQ_1:42 ;
:: thesis: verum

end;

( apply ({},((apply (p,x)) . ((len p) + 1))) = <*((apply (p,x)) . ((len p) + 1))*> & p ^ {} = p ) by Th42, FINSEQ_1:34;
then A8: S₁[ {} ] by FINSEQ_1:40;
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