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: S₁[ {} ] by Def6;
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: ( 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 A4: ( p ^ <*f*> is FuncSequence & x in firstdom (p ^ <*f*>) & x in X ) ; :: thesis: (apply (p ^ <*f*>),x) . ((len (p ^ <*f*>)) + 1) = (compose (p ^ <*f*>),X) . x
A5: apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*> by Th44;
A6: compose (p ^ <*f*>),X = f * (compose p,X) by Th43;
A7: p is FuncSequence by A4, Th62;
A8: ( len <*f*> = 1 & apply <*f*>,x = <*x,(f . x)*> & compose <*f*>,X = f * (id X) ) by Th47, Th49, FINSEQ_1:57;
( (id X) . x = x & dom (id X) = X ) by A4, FUNCT_1:34;
then A9: (f * (id X)) . x = f . x by A4, FUNCT_1:23;

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 A8, A9, FINSEQ_1:61; :: thesis: verum

end;

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

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

end;

end;

end;

for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A1, A2);
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