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 Th43;

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:47;
then A6: compose (q ^ <*f*>),X = f * (id X) by Th47;
<*f*> ^ {} = <*f*> by FINSEQ_1:47;
then firstdom (q ^ <*f*>) = dom f by A5, Th60;
hence dom (compose (q ^ <*f*>),X) = (firstdom (q ^ <*f*>)) /\ X by A6, FUNCT_1:37; :: thesis: verum

end;

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

then consider y being set , s being FinSequence such that
A8: q = <*y*> ^ s and
A9: len q = (len s) + 1 by REWRITE1:5;
q . 1 = y by A8, FINSEQ_1:58;
then A10: firstdom q = proj1 y by A8, Def6;
A11: len q >= 1 by A9, NAT_1:11;
then len q in dom q by FINSEQ_3:27;
then A12: (q ^ <*f*>) . (len q) = q . (len q) by FINSEQ_1:def 7;
A13: rng (compose q,X) c= lastrng q by A7, Th61;
consider p being FinSequence such that
len p = (len (q ^ <*f*>)) + 1 and
A14: for i being Element of NAT st i in dom (q ^ <*f*>) holds
(q ^ <*f*>) . i in Funcs (p . i),(p . (i + 1)) by A3, Def8;
consider r being FinSequence, x being set such that
A15: q = r ^ <*x*> by A7, FINSEQ_1:63;
len <*f*> = 1 by FINSEQ_1:57;
then A16: len (q ^ <*f*>) = (len q) + 1 by FINSEQ_1:35;
then len q <= len (q ^ <*f*>) by NAT_1:11;
then len q in dom (q ^ <*f*>) by A11, FINSEQ_3:27;
then A17: (q ^ <*f*>) . (len q) in Funcs (p . (len q)),(p . ((len q) + 1)) by A14;
len <*x*> = 1 by FINSEQ_1:57;
then len q = (len r) + 1 by A15, FINSEQ_1:35;
then q . (len q) = x by A15, FINSEQ_1:59;
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:58;
(len q) + 1 >= 1 by NAT_1:11;
then (len q) + 1 in dom (q ^ <*f*>) by A16, FINSEQ_3:27;
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:59;
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:45;
then A23: firstdom (q ^ <*f*>) = proj1 y by A20, Def6;
lastrng q = rng g by A15, A18, Th60;
hence dom (compose (q ^ <*f*>),X) = (firstdom (q ^ <*f*>)) /\ X by A2, A3, A4, A7, A23, A10, A19, A22, A13, Th62, RELAT_1:46, 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