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);
A1: 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 A2: 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:32
.= g * (compose ((<*f*> ^ p),X)) by Th40
.= (g * (compose (p,(f .: X)))) * (f | X) by A2, RELAT_1:36
.= (compose ((p ^ <*g*>),(f .: X))) * (f | X) by Th40 ; :: thesis: verum

end;

( <*f*> ^ {} = <*f*> & {} ^ <*f*> = <*f*> ) by FINSEQ_1:34;
then compose ((<*f*> ^ {}),X) = f * (compose ({},X)) by Th40
.= f * (id X) by Th38
.= f | X by RELAT_1:65
.= (id (rng (f | X))) * (f | X) by RELAT_1:54
.= (id (f .: X)) * (f | X) by RELAT_1:115
.= (compose ({},(f .: X))) * (f | X) by Th38 ;
then A3: S₁[ {} ] ;
for p being Function-yielding FinSequence holds S₁[p] from FUNCT_7:sch 5(A3, A1);
hence compose ((<*f*> ^ p),X) = (compose (p,(f .: X))) * (f | X) ; :: thesis: verum