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

proof

let p be Function-yielding FinSequence; :: thesis: ( S₁[p] implies for f being Function holds S₁[p ^ <*f*>] )
assume A3: apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x))) ; :: thesis: for f being Function holds S₁[p ^ <*f*>]
let g be Function; :: thesis: S₁[p ^ <*g*>]
set p9 = <*f*> ^ p;
A4: len (apply (p,(f . x))) = (len p) + 1 by Def4;
len <*f*> = 1 by FINSEQ_1:40;
then A5: len (<*f*> ^ p) = (len p) + 1 by FINSEQ_1:22;
then len (<*f*> ^ p) >= 1 by NAT_1:11;
then ( len <*x*> = 1 & len (<*f*> ^ p) in dom (apply (p,(f . x))) ) by A4, A5, FINSEQ_1:40, FINSEQ_3:25;
then A6: (apply ((<*f*> ^ p),x)) . (1 + (len (<*f*> ^ p))) = (apply (p,(f . x))) . ((len p) + 1) by A3, A5, FINSEQ_1:def 7;
apply (((<*f*> ^ p) ^ <*g*>),x) = (apply ((<*f*> ^ p),x)) ^ <*(g . ((apply ((<*f*> ^ p),x)) . ((len (<*f*> ^ p)) + 1)))*> by Th41;
hence apply ((<*f*> ^ (p ^ <*g*>)),x) = (<*x*> ^ (apply (p,(f . x)))) ^ <*(g . ((apply (p,(f . x))) . ((len p) + 1)))*> by A3, A6, FINSEQ_1:32
.= <*x*> ^ ((apply (p,(f . x))) ^ <*(g . ((apply (p,(f . x))) . ((len p) + 1)))*>) by FINSEQ_1:32
.= <*x*> ^ (apply ((p ^ <*g*>),(f . x))) by Th41 ;
:: thesis: verum

end;

( <*f*> ^ {} = <*f*> & {} ^ <*f*> = <*f*> ) by FINSEQ_1:34;
then apply ((<*f*> ^ {}),x) = (apply ({},x)) ^ <*(f . ((apply ({},x)) . (0 + 1)))*> by A1, Th41
.= <*x*> ^ <*(f . ((apply ({},x)) . 1))*> by Th39
.= <*x*> ^ <*(f . (<*x*> . 1))*> by Th39
.= <*x*> ^ <*(f . x)*>
.= <*x*> ^ (apply ({},(f . x))) by Th39 ;
then A7: S₁[ {} ] ;
for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A7, A2);
hence apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x))) ; :: thesis: verum