let x, X be set ; :: thesis: for p being FuncSequence st x in firstdom p & x in X holds
(apply p,x) . ((len p) + 1) = (compose p,X) . x
defpred S₁[ Function-yielding FinSequence] means ( $1 is FuncSequence & x in firstdom $1 & x in X implies (apply $1,x) . ((len $1) + 1) = (compose $1,X) . x );
A1: for p being Function-yielding FinSequence st S₁[p] holds
for f being Function holds S₁[p ^ <*f*>]

proof

A2: dom (id X) = X by FUNCT_1:34;
let p be Function-yielding FinSequence; :: thesis: ( S₁[p] implies for f being Function holds S₁[p ^ <*f*>] )
assume A3: ( p is FuncSequence & x in firstdom p & x in X implies (apply p,x) . ((len p) + 1) = (compose p,X) . x ) ; :: thesis: for f being Function holds S₁[p ^ <*f*>]
let f be Function; :: thesis: S₁[p ^ <*f*>]
assume that
A4: p ^ <*f*> is FuncSequence and
A5: x in firstdom (p ^ <*f*>) and
A6: x in X ; :: thesis: (apply (p ^ <*f*>),x) . ((len (p ^ <*f*>)) + 1) = (compose (p ^ <*f*>),X) . x
A7: p is FuncSequence by A4, Th62;
(id X) . x = x by A6, FUNCT_1:34;
then A8: (f * (id X)) . x = f . x by A6, A2, FUNCT_1:23;
A9: len <*f*> = 1 by FINSEQ_1:57;
A10: compose (p ^ <*f*>),X = f * (compose p,X) by Th43;
A11: ( apply <*f*>,x = <*x,(f . x)*> & compose <*f*>,X = f * (id X) ) by Th47, Th49;
A12: apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*> by Th44;

per cases ( p = {} or p <> {} ) ;

suppose p = {} ; :: thesis: (apply (p ^ <*f*>),x) . ((len (p ^ <*f*>)) + 1) = (compose (p ^ <*f*>),X) . x

then p ^ <*f*> = <*f*> by FINSEQ_1:47;
hence (apply (p ^ <*f*>),x) . ((len (p ^ <*f*>)) + 1) = (compose (p ^ <*f*>),X) . x by A9, A11, A8, FINSEQ_1:61; :: thesis: verum

end;

suppose A13: p <> {} ; :: thesis: (apply (p ^ <*f*>),x) . ((len (p ^ <*f*>)) + 1) = (compose (p ^ <*f*>),X) . x

then A14: dom (compose p,X) = (firstdom p) /\ X by A7, Th63;
A15: firstdom (p ^ <*f*>) = proj1 ((p ^ <*f*>) . 1) by Def6;
A16: firstdom p = proj1 (p . 1) by A13, Def6;
len p >= 0 + 1 by A13, NAT_1:13;
then A17: 1 in dom p by FINSEQ_3:27;
then p . 1 = (p ^ <*f*>) . 1 by FINSEQ_1:def 7;
then A18: x in (firstdom p) /\ X by A5, A6, A16, A15, XBOOLE_0:def 4;
( len (apply p,x) = (len p) + 1 & len (p ^ <*f*>) = (len p) + 1 ) by A9, Def5, FINSEQ_1:35;
hence (apply (p ^ <*f*>),x) . ((len (p ^ <*f*>)) + 1) = f . ((compose p,X) . x) by A3, A4, A5, A6, A12, A16, A15, A17, Th62, FINSEQ_1:59, FINSEQ_1:def 7
.= (compose (p ^ <*f*>),X) . x by A10, A14, A18, FUNCT_1:23 ;
:: thesis: verum

end;

end;

end;

A19: S₁[ {} ] by Def6;
for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A19, A1);
hence for p being FuncSequence st x in firstdom p & x in X holds
(apply p,x) . ((len p) + 1) = (compose p,X) . x ; :: thesis: verum