let X be set ; :: thesis: for p being FuncSequence st p <> {} holds
dom (compose (p,X)) = (firstdom p) /\ X
defpred S₁[ Function-yielding FinSequence] means ( $1 is FuncSequence & $1 <> {} implies dom (compose ($1,X)) = (firstdom $1) /\ X );
A1: for p being Function-yielding FinSequence st S₁[p] holds
for f being Function holds S₁[p ^ <*f*>]

proof

let q be Function-yielding FinSequence; :: thesis: ( S₁[q] implies for f being Function holds S₁[q ^ <*f*>] )
assume A2: ( q is FuncSequence & q <> {} implies dom (compose (q,X)) = (firstdom q) /\ X ) ; :: thesis: for f being Function holds S₁[q ^ <*f*>]
let f be Function; :: thesis: S₁[q ^ <*f*>]
assume that
A3: q ^ <*f*> is FuncSequence and
q ^ <*f*> <> {} ; :: thesis: dom (compose ((q ^ <*f*>),X)) = (firstdom (q ^ <*f*>)) /\ X
A4: compose ((q ^ <*f*>),X) = f * (compose (q,X)) by Th40;

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

suppose q = {} ; :: thesis: dom (compose ((q ^ <*f*>),X)) = (firstdom (q ^ <*f*>)) /\ X

then A5: q ^ <*f*> = <*f*> by FINSEQ_1:34;
then A6: compose ((q ^ <*f*>),X) = f * (id X) by Th44;
<*f*> ^ {} = <*f*> by FINSEQ_1:34;
then firstdom (q ^ <*f*>) = dom f by A5, Th57;
hence dom (compose ((q ^ <*f*>),X)) = (firstdom (q ^ <*f*>)) /\ X by A6, FUNCT_1:19; :: thesis: verum

end;

suppose A7: q <> {} ; :: thesis: dom (compose ((q ^ <*f*>),X)) = (firstdom (q ^ <*f*>)) /\ X

then consider y being object , s being FinSequence such that
A8: q = <*y*> ^ s and
A9: len q = (len s) + 1 by REWRITE1:5;
reconsider y = y as set by TARSKI:1;
q . 1 = y by A8, FINSEQ_1:41;
then A10: firstdom q = proj1 y by A8, Def5;
A11: len q >= 1 by A9, NAT_1:11;
then len q in dom q by FINSEQ_3:25;
then A12: (q ^ <*f*>) . (len q) = q . (len q) by FINSEQ_1:def 7;
A13: rng (compose (q,X)) c= lastrng q by A7, Th58;
consider p being FinSequence such that
len p = (len (q ^ <*f*>)) + 1 and
A14: for i being Nat st i in dom (q ^ <*f*>) holds
(q ^ <*f*>) . i in Funcs ((p . i),(p . (i + 1))) by A3, Def7;
consider r being FinSequence, x being object such that
A15: q = r ^ <*x*> by A7, FINSEQ_1:46;
len <*f*> = 1 by FINSEQ_1:40;
then A16: len (q ^ <*f*>) = (len q) + 1 by FINSEQ_1:22;
then len q <= len (q ^ <*f*>) by NAT_1:11;
then len q in dom (q ^ <*f*>) by A11, FINSEQ_3:25;
then A17: (q ^ <*f*>) . (len q) in Funcs ((p . (len q)),(p . ((len q) + 1))) by A14;
len <*x*> = 1 by FINSEQ_1:40;
then len q = (len r) + 1 by A15, FINSEQ_1:22;
then q . (len q) = x by A15, FINSEQ_1:42;
then consider g being Function such that
A18: x = g and
dom g = p . (len q) and
A19: rng g c= p . ((len q) + 1) by A17, A12, FUNCT_2:def 2;
A20: (<*y*> ^ (s ^ <*f*>)) . 1 = y by FINSEQ_1:41;
(len q) + 1 >= 1 by NAT_1:11;
then (len q) + 1 in dom (q ^ <*f*>) by A16, FINSEQ_3:25;
then A21: (q ^ <*f*>) . ((len q) + 1) in Funcs ((p . ((len q) + 1)),(p . (((len q) + 1) + 1))) by A14;
(q ^ <*f*>) . ((len q) + 1) = f by FINSEQ_1:42;
then A22: ex g being Function st
( f = g & dom g = p . ((len q) + 1) & rng g c= p . (((len q) + 1) + 1) ) by A21, FUNCT_2:def 2;
q ^ <*f*> = <*y*> ^ (s ^ <*f*>) by A8, FINSEQ_1:32;
then A23: firstdom (q ^ <*f*>) = proj1 y by A20, Def5;
lastrng q = rng g by A15, A18, Th57;
hence dom (compose ((q ^ <*f*>),X)) = (firstdom (q ^ <*f*>)) /\ X by A2, A3, A4, A7, A23, A10, A19, A22, A13, Th59, RELAT_1:27, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

A24: S₁[ {} ] ;
for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A24, A1);
hence for p being FuncSequence st p <> {} holds
dom (compose (p,X)) = (firstdom p) /\ X ; :: thesis: verum