let X be set ; :: thesis: for p being Function-yielding FinSequence
for f being Function holds compose (<*f*> ^ p),X = (compose p,(f .: X)) * (f | X)
let p be Function-yielding FinSequence; :: thesis: for f being Function holds compose (<*f*> ^ p),X = (compose p,(f .: X)) * (f | X)
let f be Function; :: thesis: compose (<*f*> ^ p),X = (compose p,(f .: X)) * (f | X)
defpred S₁[ Function-yielding FinSequence] means compose (<*f*> ^ $1),X = (compose $1,(f .: X)) * (f | X);
( <*f*> ^ {} = <*f*> & {} ^ <*f*> = <*f*> ) by FINSEQ_1:47;
then compose (<*f*> ^ {} ),X = f * (compose {} ,X) by Th43
.= f * (id X) by Th41
.= f | X by RELAT_1:94
.= (id (rng (f | X))) * (f | X) by RELAT_1:80
.= (id (f .: X)) * (f | X) by RELAT_1:148
.= (compose {} ,(f .: X)) * (f | X) by Th41 ;
then A1: S₁[ {} ] ;
A2: for p being Function-yielding FinSequence st S₁[p] holds
for f being Function holds S₁[p ^ <*f*>]

proof

let p be Function-yielding FinSequence; :: thesis: ( S₁[p] implies for f being Function holds S₁[p ^ <*f*>] )
assume A3: compose (<*f*> ^ p),X = (compose p,(f .: X)) * (f | X) ; :: thesis: for f being Function holds S₁[p ^ <*f*>]
let g be Function; :: thesis: S₁[p ^ <*g*>]
thus compose (<*f*> ^ (p ^ <*g*>)),X = compose ((<*f*> ^ p) ^ <*g*>),X by FINSEQ_1:45
.= g * (compose (<*f*> ^ p),X) by Th43
.= (g * (compose p,(f .: X))) * (f | X) by A3, RELAT_1:55
.= (compose (p ^ <*g*>),(f .: X)) * (f | X) by Th43 ; :: thesis: verum

end;

for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A1, A2);
hence compose (<*f*> ^ p),X = (compose p,(f .: X)) * (f | X) ; :: thesis: verum