let X be set ; :: thesis: for p being Function-yielding FinSequence
for f being Function holds compose ((p ^ <*f*>),X) = f * (compose (p,X))
let p be Function-yielding FinSequence; :: thesis: for f being Function holds compose ((p ^ <*f*>),X) = f * (compose (p,X))
let f be Function; :: thesis: compose ((p ^ <*f*>),X) = f * (compose (p,X))
A1: f = (p ^ <*f*>) . ((len p) + 1) by FINSEQ_1:42;
len <*f*> = 1 by FINSEQ_1:40;
then A2: len (p ^ <*f*>) = (len p) + 1 by FINSEQ_1:22;
consider ff being ManySortedFunction of NAT such that
A3: compose ((p ^ <*f*>),X) = ff . (len (p ^ <*f*>)) and
A4: ff . 0 = id X and
A5: for i being Nat st i + 1 in dom (p ^ <*f*>) holds
for g, h being Function st g = ff . i & h = (p ^ <*f*>) . (i + 1) holds
ff . (i + 1) = h * g by Def3;
reconsider g = ff . (len p) as Function ;
A6: dom p c= dom (p ^ <*f*>) by FINSEQ_1:26;

now :: thesis: for i being Nat st i + 1 in dom p holds
for g, h being Function st g = ff . i & h = p . (i + 1) holds
ff . (i + 1) = h * g

let i be Nat; :: thesis: ( i + 1 in dom p implies for g, h being Function st g = ff . i & h = p . (i + 1) holds
ff . (i + 1) = h * g )
assume A7: i + 1 in dom p ; :: thesis: for g, h being Function st g = ff . i & h = p . (i + 1) holds
ff . (i + 1) = h * g
let g, h be Function; :: thesis: ( g = ff . i & h = p . (i + 1) implies ff . (i + 1) = h * g )
assume that
A8: g = ff . i and
A9: h = p . (i + 1) ; :: thesis: ff . (i + 1) = h * g
h = (p ^ <*f*>) . (i + 1) by A7, A9, FINSEQ_1:def 7;
hence ff . (i + 1) = h * g by A5, A6, A7, A8; :: thesis: verum

end;

then A10: g = compose (p,X) by A4, Def3;
( 1 in Seg 1 & dom <*f*> = Seg 1 ) by FINSEQ_1:2, FINSEQ_1:38, TARSKI:def 1;
hence compose ((p ^ <*f*>),X) = f * (compose (p,X)) by A3, A5, A10, A2, A1, FINSEQ_1:28; :: thesis: verum