let x be object ; :: 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 Def4;
then consider r being FinSequence, y being object such that
A2: apply (p,x) = r ^ <*y*> by CARD_1:27, FINSEQ_1:46;
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 Th48;
let f be Function; :: thesis: S₁[q ^ <*f*>]
A6: len (apply (q,((apply (p,x)) . ((len p) + 1)))) = (len q) + 1 by Def4;
A7: len (apply ((q ^ <*f*>),((apply (p,x)) . ((len p) + 1)))) = (len (q ^ <*f*>)) + 1 by Def4;
thus apply ((p ^ (q ^ <*f*>)),x) = apply (((p ^ q) ^ <*f*>),x) by FINSEQ_1:32
.= (apply ((p ^ q),x)) ^ <*(f . ((apply ((p ^ q),x)) . ((len (p ^ q)) + 1)))*> by Th41
.= (r ^ (apply (q,((apply (p,x)) . ((len p) + 1))))) ^ <*(f . ((apply ((p ^ q),x)) . ((len (p ^ q)) + 1)))*> by A2, A4, A6, CARD_1:27, REWRITE1:2
.= r ^ ((apply (q,((apply (p,x)) . ((len p) + 1)))) ^ <*(f . ((apply ((p ^ q),x)) . ((len (p ^ q)) + 1)))*>) by FINSEQ_1:32
.= r ^ (apply ((q ^ <*f*>),((apply (p,x)) . ((len p) + 1)))) by A5, Th41
.= (apply (p,x)) $^ (apply ((q ^ <*f*>),((apply (p,x)) . ((len p) + 1)))) by A2, A7, CARD_1:27, REWRITE1:2 ; :: thesis: verum

end;

len <*y*> = 1 by FINSEQ_1:40;
then (len p) + 1 = (len r) + 1 by A1, A2, FINSEQ_1:22;
then A8: (apply (p,x)) . ((len p) + 1) = y by A2, FINSEQ_1:42;
apply ((p ^ {}),x) = apply (p,x) by FINSEQ_1:34
.= (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 Th39 ;
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