let X be set ; :: thesis: for p being Function-yielding FinSequence st p <> {} holds
rng (compose (p,X)) c= lastrng p
defpred S₁[ Function-yielding FinSequence] means ( $1 <> {} implies rng (compose ($1,X)) c= lastrng $1 );
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 ( q <> {} implies rng (compose (q,X)) c= lastrng q ) ; :: thesis: for f being Function holds S₁[q ^ <*f*>]
let f be Function; :: thesis: S₁[q ^ <*f*>]
assume q ^ <*f*> <> {} ; :: thesis: rng (compose ((q ^ <*f*>),X)) c= lastrng (q ^ <*f*>)
compose ((q ^ <*f*>),X) = f * (compose (q,X)) by Th40;
then rng (compose ((q ^ <*f*>),X)) c= rng f by RELAT_1:26;
hence rng (compose ((q ^ <*f*>),X)) c= lastrng (q ^ <*f*>) by Th57; :: thesis: verum

end;

A2: S₁[ {} ] ;
thus for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A2, A1); :: thesis: verum