let x be set ; :: thesis: for p, q being Function-yielding FinSequence holds (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)
let p, q be Function-yielding FinSequence; :: thesis: (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)
defpred S1[ Function-yielding FinSequence] means (apply (p ^ $1),x) . ((len (p ^ $1)) + 1) = (apply $1,((apply p,x) . ((len p) + 1))) . ((len $1) + 1);
( apply {} ,((apply p,x) . ((len p) + 1)) = <*((apply p,x) . ((len p) + 1))*> & p ^ {} = p )
by Th42, FINSEQ_1:47;
then A1:
S1[ {} ]
by FINSEQ_1:57;
A2:
for p being Function-yielding FinSequence st S1[p] holds
for f being Function holds S1[p ^ <*f*>]
proof
let q be
Function-yielding FinSequence;
:: thesis: ( S1[q] implies for f being Function holds S1[q ^ <*f*>] )
assume A3:
(apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)
;
:: thesis: for f being Function holds S1[q ^ <*f*>]
let f be
Function;
:: thesis: S1[q ^ <*f*>]
A4:
p ^ (q ^ <*f*>) = (p ^ q) ^ <*f*>
by FINSEQ_1:45;
A5:
apply ((p ^ q) ^ <*f*>),
x = (apply (p ^ q),x) ^ <*(f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1)))*>
by Th44;
A6:
len <*f*> = 1
by FINSEQ_1:57;
then A7:
(
len (apply (p ^ q),x) = (len (p ^ q)) + 1 &
len ((p ^ q) ^ <*f*>) = (len (p ^ q)) + 1 )
by Def5, FINSEQ_1:35;
set y =
(apply p,x) . ((len p) + 1);
A8:
apply (q ^ <*f*>),
((apply p,x) . ((len p) + 1)) = (apply q,((apply p,x) . ((len p) + 1))) ^ <*(f . ((apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)))*>
by Th44;
A9:
(
len (apply q,((apply p,x) . ((len p) + 1))) = (len q) + 1 &
len (q ^ <*f*>) = (len q) + 1 )
by A6, Def5, FINSEQ_1:35;
thus (apply (p ^ (q ^ <*f*>)),x) . ((len (p ^ (q ^ <*f*>))) + 1) =
f . ((apply (p ^ q),x) . ((len (p ^ q)) + 1))
by A4, A5, A7, FINSEQ_1:59
.=
(apply (q ^ <*f*>),((apply p,x) . ((len p) + 1))) . ((len (q ^ <*f*>)) + 1)
by A3, A8, A9, FINSEQ_1:59
;
:: thesis: verum
end;
for q being Function-yielding FinSequence holds S1[q]
from FUNCT_7:sch 5(A1, A2);
hence
(apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)
; :: thesis: verum