let X be set ; :: thesis: for x being object
for p being FuncSequence st x in firstdom p & x in X holds
(apply (p,x)) . ((len p) + 1) = (compose (p,X)) . x
let x be object ; :: 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 ;
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, Th59;
(id X) . x = x by A6, FUNCT_1:17;
then A8: (f * (id X)) . x = f . x by A6, A2, FUNCT_1:13;
A9: len <*f*> = 1 by FINSEQ_1:40;
A10: compose ((p ^ <*f*>),X) = f * (compose (p,X)) by Th40;
A11: ( apply (<*f*>,x) = <*x,(f . x)*> & compose (<*f*>,X) = f * (id X) ) by Th44, Th46;
A12: apply ((p ^ <*f*>),x) = (apply (p,x)) ^ <*(f . ((apply (p,x)) . ((len p) + 1)))*> by Th41;

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:34;
hence (apply ((p ^ <*f*>),x)) . ((len (p ^ <*f*>)) + 1) = (compose ((p ^ <*f*>),X)) . x by A9, A11, A8; :: 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, Th60;
A15: firstdom (p ^ <*f*>) = proj1 ((p ^ <*f*>) . 1) by Def5;
A16: firstdom p = proj1 (p . 1) by A13, Def5;
len p >= 0 + 1 by A13, NAT_1:13;
then A17: 1 in dom p by FINSEQ_3:25;
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, Def4, FINSEQ_1:22;
hence (apply ((p ^ <*f*>),x)) . ((len (p ^ <*f*>)) + 1) = f . ((compose (p,X)) . x) by A3, A4, A5, A6, A12, A16, A15, A17, Th59, FINSEQ_1:42, FINSEQ_1:def 7
.= (compose ((p ^ <*f*>),X)) . x by A10, A14, A18, FUNCT_1:13 ;
:: thesis: verum

end;

end;

end;

A19: S₁[ {} ] by Def5;
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