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:45
.= f * (compose (p ^ q),X) by Th43
.= (f * (compose q,Y)) * (compose p,X) by A3, RELAT_1:55
.= (compose (q ^ <*f*>),Y) * (compose p,X) by Th43 ; :: thesis: verum

end;

compose (p ^ {} ),X = compose p,X by FINSEQ_1:47
.= (id Y) * (compose p,X) by A1, RELAT_1:79
.= (compose {} ,Y) * (compose p,X) by Th41 ;
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