let x be set ; :: 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 Def5;
len <*f*> = 1 by FINSEQ_1:57;
then A5: len (<*f*> ^ p) = (len p) + 1 by FINSEQ_1:35;
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:57, FINSEQ_3:27;
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 Th44;
hence apply (<*f*> ^ (p ^ <*g*>)),x = (<*x*> ^ (apply p,(f . x))) ^ <*(g . ((apply p,(f . x)) . ((len p) + 1)))*> by A3, A6, FINSEQ_1:45
.= <*x*> ^ ((apply p,(f . x)) ^ <*(g . ((apply p,(f . x)) . ((len p) + 1)))*>) by FINSEQ_1:45
.= <*x*> ^ (apply (p ^ <*g*>),(f . x)) by Th44 ;
:: thesis: verum

end;

( <*f*> ^ {} = <*f*> & {} ^ <*f*> = <*f*> ) by FINSEQ_1:47;
then apply (<*f*> ^ {} ),x = (apply {} ,x) ^ <*(f . ((apply {} ,x) . (0 + 1)))*> by A1, Th44
.= <*x*> ^ <*(f . ((apply {} ,x) . 1))*> by Th42
.= <*x*> ^ <*(f . (<*x*> . 1))*> by Th42
.= <*x*> ^ <*(f . x)*> by FINSEQ_1:57
.= <*x*> ^ (apply {} ,(f . x)) by Th42 ;
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