let X, Y be set ; :: thesis: for p, q being Function-yielding FinSequence st rng (compose (p,X)) c= Y holds
compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X))
let p, q be Function-yielding FinSequence; :: thesis: ( rng (compose (p,X)) c= Y implies compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X)) )
assume A1: rng (compose (p,X)) c= Y ; :: thesis: compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X))
defpred S₁[ Function-yielding FinSequence] means compose ((p ^ $1),X) = (compose ($1,Y)) * (compose (p,X));
A2: 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 A3: compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X)) ; :: thesis: for f being Function holds S₁[q ^ <*f*>]
let f be Function; :: thesis: S₁[q ^ <*f*>]
thus compose ((p ^ (q ^ <*f*>)),X) = compose (((p ^ q) ^ <*f*>),X) by FINSEQ_1:32
.= f * (compose ((p ^ q),X)) by Th40
.= (f * (compose (q,Y))) * (compose (p,X)) by A3, RELAT_1:36
.= (compose ((q ^ <*f*>),Y)) * (compose (p,X)) by Th40 ; :: thesis: verum

end;

compose ((p ^ {}),X) = compose (p,X) by FINSEQ_1:34
.= (id Y) * (compose (p,X)) by A1, RELAT_1:53
.= (compose ({},Y)) * (compose (p,X)) by Th38 ;
then A4: S₁[ {} ] ;
for q being Function-yielding FinSequence holds S₁[q] from FUNCT_7:sch 5(A4, A2);
hence compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X)) ; :: thesis: verum