let x be object ; 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; for f being Function holds apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x)))
let f be Function; apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x)))
defpred S1[ Function-yielding FinSequence] means apply ((<*f*> ^ $1),x) = <*x*> ^ (apply ($1,(f . x)));
A1:
len {} = 0
;
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;
( S1[p] implies for f being Function holds S1[p ^ <*f*>] )
assume A3:
apply (
(<*f*> ^ p),
x)
= <*x*> ^ (apply (p,(f . x)))
;
for f being Function holds S1[p ^ <*f*>]
let g be
Function;
S1[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
;
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)*>
by FINSEQ_1:40
.=
<*x*> ^ (apply ({},(f . x)))
by Th39
;
then A7:
S1[ {} ]
;
for p being Function-yielding FinSequence holds S1[p]
from FUNCT_7:sch 5(A7, A2);
hence
apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x)))
; verum