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 S1[ Function-yielding FinSequence] means apply (<*f*> ^ $1),x = <*x*> ^ (apply $1,(f . x));
( <*f*> ^ {} = <*f*> & {} ^ <*f*> = <*f*> & len {} = 0 )
by FINSEQ_1:47;
then apply (<*f*> ^ {} ),x =
(apply {} ,x) ^ <*(f . ((apply {} ,x) . (0 + 1)))*>
by 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 A1:
S1[ {} ]
;
A2:
for p being Function-yielding FinSequence st S1[p] holds
for f being Function holds S1[p ^ <*f*>]
proof
let p be
Function-yielding FinSequence;
:: thesis: ( S1[p] implies for f being Function holds S1[p ^ <*f*>] )
assume A3:
apply (<*f*> ^ p),
x = <*x*> ^ (apply p,(f . x))
;
:: thesis: for f being Function holds S1[p ^ <*f*>]
let g be
Function;
:: thesis: S1[p ^ <*g*>]
set p' =
<*f*> ^ p;
A4:
apply ((<*f*> ^ p) ^ <*g*>),
x = (apply (<*f*> ^ p),x) ^ <*(g . ((apply (<*f*> ^ p),x) . ((len (<*f*> ^ p)) + 1)))*>
by Th44;
A5:
(
len <*x*> = 1 &
len <*f*> = 1 )
by FINSEQ_1:57;
then A6:
(
len (apply p,(f . x)) = (len p) + 1 &
len (<*f*> ^ p) = (len p) + 1 )
by Def5, FINSEQ_1:35;
then
len (<*f*> ^ p) >= 1
by NAT_1:11;
then
len (<*f*> ^ p) in dom (apply p,(f . x))
by A6, FINSEQ_3:27;
then
(apply (<*f*> ^ p),x) . (1 + (len (<*f*> ^ p))) = (apply p,(f . x)) . ((len p) + 1)
by A3, A5, A6, FINSEQ_1:def 7;
hence apply (<*f*> ^ (p ^ <*g*>)),
x =
(<*x*> ^ (apply p,(f . x))) ^ <*(g . ((apply p,(f . x)) . ((len p) + 1)))*>
by A3, A4, 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;
for p being Function-yielding FinSequence holds S1[p]
from FUNCT_7:sch 5(A1, A2);
hence
apply (<*f*> ^ p),x = <*x*> ^ (apply p,(f . x))
; :: thesis: verum